Theorem 3com23 1197

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

Syntax hints:   -> wi 4   /\ w3a 968

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 371  df-3an 970

This theorem is referenced by:  3coml  1198  syld3an2  1270  3anidm13  1281  eqreu  3288  f1ofveu  6270  curry2f  6869  dfsmo2  7008  nneob  7291  f1oeng  7524  suppr  7918  infdif  8578  axdclem2  8889  gchen1  8992  grumap  9175  grudomon  9184  mul32  9735  add32  9782  subsub23  9814  subadd23  9821  addsub12  9822  subsub  9838  subsub3  9840  sub32  9842  suble  10019  lesub  10020  ltsub23  10021  ltsub13  10022  ltleadd  10024  div32  10216  div13  10217  div12  10218  divdiv32  10241  cju  10521  infmssuzle  11153  ioo0  11543  ico0  11564  ioc0  11565  icc0  11566  fzen  11692  elfz1b  11737  elfzmlbm  11771  modcyc  11987  expgt0  12154  expge0  12157  expge1  12158  2cshwcom  12734  shftval2  12858  abs3dif  13113  divalgb  13910  submrc  14872  mrieqv2d  14883  pltnlt  15444  pltn2lp  15445  tosso  15512  latnle  15561  latabs1  15563  lubel  15598  ipopos  15636  grpinvcnv  15900  mulgneg2  15962  oppgmnd  16177  oddvdsnn0  16357  oddvds  16360  odmulg  16367  odcl2  16376  lsmcomx  16648  srgrmhm  16968  rngcom  17007  mulgass2  17026  opprrng  17057  irredrmul  17133  irredlmul  17134  isdrngrd  17198  islmodd  17294  lmodcom  17332  opprdomn  17714  zntoslem  18355  ipcl  18428  maducoevalmin1  18914  rintopn  19178  opnnei  19380  restin  19426  cnpnei  19524  cnprest  19549  ordthaus  19644  kgen2ss  19784  hausflim  20210  fclsfnflim  20256  cnpfcf  20270  opnsubg  20334  cuspcvg  20532  psmetsym  20542  xmetsym  20578  ngpdsr  20852  ngpds2r  20854  ngpds3r  20856  clmmulg  21321  iscau2  21444  dgr1term  22384  cxpeq0  22780  cxpge0  22785  grpoidinvlem2  24733  grpoinvdiv  24773  gxcl  24793  nvpncan  25078  nvsub  25096  nvabs  25102  nvelbl  25125  ipval2lem2  25140  ipval2lem5  25146  dipcj  25153  diporthcom  25155  dipdi  25284  dipassr  25287  dipsubdi  25290  hlipcj  25353  hvadd32  25477  hvsub32  25488  his5  25529  hoadd32  26228  hosubsub  26262  unopf1o  26361  adj2  26379  adjvalval  26382  adjlnop  26531  leopmul2i  26580  cvntr  26737  mdsymlem5  26852  sumdmdii  26860  supxrnemnf  27101  odutos  27163  tlt2  27164  tosglblem  27169  archiabl  27254  unitdivcld  27369  ghomf1olem  28359  gcd32  28603  cgrrflx  29064  cgrcom  29067  cgrcomr  29074  btwntriv1  29093  cgr3com  29130  colineartriv2  29145  segleantisym  29192  seglelin  29193  btwnoutside  29202  ftc1anclem5  29522  clsint2  29575  heibor1  29760  rngoidl  29875  ispridlc  29921  nerabdioph  30197  monotoddzzfi  30333  fzneg  30375  jm2.19lem2  30389  lincvalsng  31965  reccot  32108  sineq0ALT  32692  bnj605  32919  bnj607  32928  opltcon3b  33876  cmtcomlemN  33920  cmtcomN  33921  cmt3N  33923  cmtbr3N  33926  cvrval2  33946  cvrnbtwn4  33951  leatb  33964  atlrelat1  33993  hlatlej2  34047  hlateq  34070  hlrelat5N  34072  snatpsubN  34421  pmap11  34433  paddcom  34484  sspadd2  34487  paddss12  34490  cdleme51finvN  35227  cdleme51finvtrN  35229  cdlemeiota  35256  cdlemg2jlemOLDN  35264  cdlemg2klem  35266  cdlemg4b1  35280  cdlemg4b2  35281  trljco2  35412  tgrpabl  35422  tendoplcom  35453  cdleml6  35652  erngdvlem3-rN  35669  dia11N  35720  dib11N  35832  dih11  35937