Theorem 3com23 1211

Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
3com23	|- ( ( ph /\ ch /\ ps ) -> th )

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 |- ( ( ph /\ ps /\ ch ) -> th )
2	1	3exp 1204	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 81	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1199	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984

This theorem is referenced by:  3coml  1212  syld3an2  1311  3anidm13  1322  eqreu  3260  f1ofveu  6291  curry2f  6894  dfsmo2  7065  nneob  7352  f1oeng  7586  suppr  7984  infdif  8628  axdclem2  8939  gchen1  9039  grumap  9222  grudomon  9231  mul32  9789  add32  9836  subsub23  9869  subadd23  9876  addsub12  9877  subsub  9893  subsub3  9895  sub32  9897  suble  10081  lesub  10082  ltsub23  10083  ltsub13  10084  ltleadd  10086  div32  10279  div13  10280  div12  10281  divdiv32  10304  cju  10594  infssuzle  11233  infmssuzleOLD  11235  ioo0  11650  ico0  11671  ioc0  11672  icc0  11673  fzen  11803  elfz1b  11851  elfzmlbmOLD  11888  modcyc  12118  expgt0  12291  expge0  12294  expge1  12295  2cshwcom  12889  shftval2  13106  abs3dif  13362  divalgb  14349  submrc  15478  mrieqv2d  15489  pltnlt  16158  pltn2lp  16159  tosso  16226  latnle  16275  latabs1  16277  lubel  16312  ipopos  16350  grpinvcnv  16666  mulgneg2  16729  oppgmnd  16949  oddvdsnn0  17128  oddvds  17131  odmulg  17138  odcl2  17147  lsmcomx  17422  srgrmhm  17697  ringcom  17737  mulgass2  17757  opprring  17787  irredrmul  17863  irredlmul  17864  isdrngrd  17929  islmodd  18025  lmodcom  18062  opprdomn  18453  zntoslem  19051  ipcl  19124  maducoevalmin1  19601  rintopn  19863  opnnei  20060  restin  20106  cnpnei  20204  cnprest  20229  ordthaus  20324  kgen2ss  20494  hausflim  20920  fclsfnflim  20966  cnpfcf  20980  opnsubg  21046  cuspcvg  21240  psmetsym  21250  xmetsym  21286  ngpdsr  21542  ngpds2r  21544  ngpds3r  21546  clmmulg  22010  iscau2  22133  dgr1term  23079  cxpeq0  23485  cxpge0  23490  relogbzcl  23573  grpoidinvlem2  25775  grpoinvdiv  25815  gxcl  25835  nvpncan  26120  nvsub  26138  nvabs  26144  nvelbl  26167  ipval2lem2  26182  ipval2lem5  26188  dipcj  26195  diporthcom  26197  dipdi  26326  dipassr  26329  dipsubdi  26332  hlipcj  26395  hvadd32  26519  hvsub32  26530  his5  26571  hoadd32  27268  hosubsub  27302  unopf1o  27401  adj2  27419  adjvalval  27422  adjlnop  27571  leopmul2i  27620  cvntr  27777  mdsymlem5  27892  sumdmdii  27900  supxrnemnf  28187  odutos  28259  tlt2  28260  tosglblem  28265  archiabl  28350  unitdivcld  28543  bnj605  29503  bnj607  29512  ghomf1olem  30097  gcd32  30171  cgrrflx  30536  cgrcom  30539  cgrcomr  30546  btwntriv1  30565  cgr3com  30602  colineartriv2  30617  segleantisym  30664  seglelin  30665  btwnoutside  30674  clsint2  30767  dissneqlem  31473  ftc1anclem5  31725  heibor1  31846  rngoidl  31961  ispridlc  32007  opltcon3b  32479  cmtcomlemN  32523  cmtcomN  32524  cmt3N  32526  cmtbr3N  32529  cvrval2  32549  cvrnbtwn4  32554  leatb  32567  atlrelat1  32596  hlatlej2  32650  hlateq  32673  hlrelat5N  32675  snatpsubN  33024  pmap11  33036  paddcom  33087  sspadd2  33090  paddss12  33093  cdleme51finvN  33832  cdleme51finvtrN  33834  cdlemeiota  33861  cdlemg2jlemOLDN  33869  cdlemg2klem  33871  cdlemg4b1  33885  cdlemg4b2  33886  trljco2  34017  tgrpabl  34027  tendoplcom  34058  cdleml6  34257  erngdvlem3-rN  34274  dia11N  34325  dib11N  34437  dih11  34542  nerabdioph  35361  monotoddzzfi  35500  fzneg  35542  jm2.19lem2  35555  nzss  36307  sineq0ALT  36978  lincvalsng  38982  reccot  39252