Theorem 3com23 1200

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 1193	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1188	1 |- ( ( ph /\ ch /\ ps ) -> th )

Syntax hints:   -> wi 4   /\ w3a 971

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 185  df-an 369  df-3an 973

This theorem is referenced by:  3coml  1201  syld3an2  1273  3anidm13  1284  eqreu  3288  f1ofveu  6265  curry2f  6869  dfsmo2  7010  nneob  7293  f1oeng  7527  suppr  7921  infdif  8580  axdclem2  8891  gchen1  8992  grumap  9175  grudomon  9184  mul32  9736  add32  9783  subsub23  9816  subadd23  9823  addsub12  9824  subsub  9840  subsub3  9842  sub32  9844  suble  10026  lesub  10027  ltsub23  10028  ltsub13  10029  ltleadd  10031  div32  10223  div13  10224  div12  10225  divdiv32  10248  cju  10527  infmssuzle  11165  ioo0  11557  ico0  11578  ioc0  11579  icc0  11580  fzen  11706  elfz1b  11752  elfzmlbmOLD  11789  modcyc  12013  expgt0  12181  expge0  12184  expge1  12185  2cshwcom  12775  shftval2  12990  abs3dif  13246  divalgb  14146  submrc  15117  mrieqv2d  15128  pltnlt  15797  pltn2lp  15798  tosso  15865  latnle  15914  latabs1  15916  lubel  15951  ipopos  15989  grpinvcnv  16305  mulgneg2  16368  oppgmnd  16588  oddvdsnn0  16767  oddvds  16770  odmulg  16777  odcl2  16786  lsmcomx  17061  srgrmhm  17382  ringcom  17422  mulgass2  17442  opprring  17475  irredrmul  17551  irredlmul  17552  isdrngrd  17617  islmodd  17713  lmodcom  17751  opprdomn  18145  zntoslem  18768  ipcl  18841  maducoevalmin1  19321  rintopn  19585  opnnei  19788  restin  19834  cnpnei  19932  cnprest  19957  ordthaus  20052  kgen2ss  20222  hausflim  20648  fclsfnflim  20694  cnpfcf  20708  opnsubg  20772  cuspcvg  20970  psmetsym  20980  xmetsym  21016  ngpdsr  21290  ngpds2r  21292  ngpds3r  21294  clmmulg  21759  iscau2  21882  dgr1term  22823  cxpeq0  23227  cxpge0  23232  relogbzcl  23313  grpoidinvlem2  25405  grpoinvdiv  25445  gxcl  25465  nvpncan  25750  nvsub  25768  nvabs  25774  nvelbl  25797  ipval2lem2  25812  ipval2lem5  25818  dipcj  25825  diporthcom  25827  dipdi  25956  dipassr  25959  dipsubdi  25962  hlipcj  26025  hvadd32  26149  hvsub32  26160  his5  26201  hoadd32  26900  hosubsub  26934  unopf1o  27033  adj2  27051  adjvalval  27054  adjlnop  27203  leopmul2i  27252  cvntr  27409  mdsymlem5  27524  sumdmdii  27532  supxrnemnf  27817  odutos  27885  tlt2  27886  tosglblem  27891  archiabl  27976  unitdivcld  28118  ghomf1olem  29298  gcd32  29417  cgrrflx  29865  cgrcom  29868  cgrcomr  29875  btwntriv1  29894  cgr3com  29931  colineartriv2  29946  segleantisym  29993  seglelin  29994  btwnoutside  30003  ftc1anclem5  30334  clsint2  30387  heibor1  30546  rngoidl  30661  ispridlc  30707  nerabdioph  30982  monotoddzzfi  31117  fzneg  31159  jm2.19lem2  31171  nzss  31463  lincvalsng  33271  reccot  33542  sineq0ALT  34138  bnj605  34366  bnj607  34375  opltcon3b  35326  cmtcomlemN  35370  cmtcomN  35371  cmt3N  35373  cmtbr3N  35376  cvrval2  35396  cvrnbtwn4  35401  leatb  35414  atlrelat1  35443  hlatlej2  35497  hlateq  35520  hlrelat5N  35522  snatpsubN  35871  pmap11  35883  paddcom  35934  sspadd2  35937  paddss12  35940  cdleme51finvN  36679  cdleme51finvtrN  36681  cdlemeiota  36708  cdlemg2jlemOLDN  36716  cdlemg2klem  36718  cdlemg4b1  36732  cdlemg4b2  36733  trljco2  36864  tgrpabl  36874  tendoplcom  36905  cdleml6  37104  erngdvlem3-rN  37121  dia11N  37172  dib11N  37284  dih11  37389