Theorem 3com23 1214

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 1207	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 81	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1202	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 985

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 189  df-an 373  df-3an 987

This theorem is referenced by:  3coml  1215  syld3an2  1315  3anidm13  1326  eqreu  3230  f1ofveu  6285  curry2f  6892  dfsmo2  7066  nneob  7353  f1oeng  7588  suppr  7987  infdif  8639  axdclem2  8950  gchen1  9050  grumap  9233  grudomon  9242  mul32  9800  add32  9847  subsub23  9880  subadd23  9887  addsub12  9888  subsub  9904  subsub3  9906  sub32  9908  suble  10092  lesub  10093  ltsub23  10094  ltsub13  10095  ltleadd  10097  div32  10290  div13  10291  div12  10292  divdiv32  10315  cju  10605  infssuzle  11244  infmssuzleOLD  11246  ioo0  11661  ico0  11682  ioc0  11683  icc0  11684  fzen  11816  elfz1b  11864  elfzmlbmOLD  11901  modcyc  12132  expgt0  12305  expge0  12308  expge1  12309  2cshwcom  12915  shftval2  13138  abs3dif  13394  divalgb  14385  submrc  15534  mrieqv2d  15545  pltnlt  16214  pltn2lp  16215  tosso  16282  latnle  16331  latabs1  16333  lubel  16368  ipopos  16406  grpinvcnv  16722  mulgneg2  16785  oppgmnd  17005  oddvdsnn0  17193  oddvds  17196  odmulg  17207  odcl2  17216  lsmcomx  17494  srgrmhm  17769  ringcom  17809  mulgass2  17829  opprring  17859  irredrmul  17935  irredlmul  17936  isdrngrd  18001  islmodd  18097  lmodcom  18134  opprdomn  18525  zntoslem  19127  ipcl  19200  maducoevalmin1  19677  rintopn  19939  opnnei  20136  restin  20182  cnpnei  20280  cnprest  20305  ordthaus  20400  kgen2ss  20570  hausflim  20996  fclsfnflim  21042  cnpfcf  21056  opnsubg  21122  cuspcvg  21316  psmetsym  21326  xmetsym  21362  ngpdsr  21618  ngpds2r  21620  ngpds3r  21622  clmmulg  22124  iscau2  22247  dgr1term  23214  cxpeq0  23623  cxpge0  23628  relogbzcl  23711  grpoidinvlem2  25933  grpoinvdiv  25973  gxcl  25993  nvpncan  26278  nvsub  26296  nvabs  26302  nvelbl  26325  ipval2lem2  26340  ipval2lem5  26346  dipcj  26353  diporthcom  26355  dipdi  26484  dipassr  26487  dipsubdi  26490  hlipcj  26563  hvadd32  26687  hvsub32  26698  his5  26739  hoadd32  27436  hosubsub  27470  unopf1o  27569  adj2  27587  adjvalval  27590  adjlnop  27739  leopmul2i  27788  cvntr  27945  mdsymlem5  28060  sumdmdii  28068  supxrnemnf  28354  odutos  28424  tlt2  28425  tosglblem  28430  archiabl  28515  unitdivcld  28707  bnj605  29718  bnj607  29727  ghomf1olem  30312  gcd32  30387  cgrrflx  30754  cgrcom  30757  cgrcomr  30764  btwntriv1  30783  cgr3com  30820  colineartriv2  30835  segleantisym  30882  seglelin  30883  btwnoutside  30892  clsint2  30985  dissneqlem  31742  ftc1anclem5  32021  heibor1  32142  rngoidl  32257  ispridlc  32303  opltcon3b  32770  cmtcomlemN  32814  cmtcomN  32815  cmt3N  32817  cmtbr3N  32820  cvrval2  32840  cvrnbtwn4  32845  leatb  32858  atlrelat1  32887  hlatlej2  32941  hlateq  32964  hlrelat5N  32966  snatpsubN  33315  pmap11  33327  paddcom  33378  sspadd2  33381  paddss12  33384  cdleme51finvN  34123  cdleme51finvtrN  34125  cdlemeiota  34152  cdlemg2jlemOLDN  34160  cdlemg2klem  34162  cdlemg4b1  34176  cdlemg4b2  34177  trljco2  34308  tgrpabl  34318  tendoplcom  34349  cdleml6  34548  erngdvlem3-rN  34565  dia11N  34616  dib11N  34728  dih11  34833  nerabdioph  35652  monotoddzzfi  35790  fzneg  35832  jm2.19lem2  35845  nzss  36666  sineq0ALT  37334  lincvalsng  40262  reccot  40531