Theorem 3com23 1194

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

Syntax hints:   -> wi 4   /\ w3a 965

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 967

This theorem is referenced by:  3coml  1195  syld3an2  1266  3anidm13  1277  eqreu  3248  f1ofveu  6185  curry2f  6768  dfsmo2  6908  nneob  7191  f1oeng  7428  suppr  7819  infdif  8479  axdclem2  8790  gchen1  8893  grumap  9076  grudomon  9085  mul32  9637  add32  9684  subsub23  9716  subadd23  9723  addsub12  9724  subsub  9740  subsub3  9742  sub32  9744  suble  9918  lesub  9919  ltsub23  9920  ltsub13  9921  ltleadd  9923  div32  10115  div13  10116  div12  10117  divdiv32  10140  cju  10419  infmssuzle  11038  ioo0  11426  ico0  11447  ioc0  11448  icc0  11449  fzen  11568  elfzmlbm  11591  elfz1b  11628  modcyc  11844  expgt0  11998  expge0  12001  expge1  12002  2cshwcom  12552  shftval2  12666  abs3dif  12921  divalgb  13710  submrc  14668  mrieqv2d  14679  pltnlt  15240  pltn2lp  15241  tosso  15308  latnle  15357  latabs1  15359  lubel  15394  ipopos  15432  grpinvcnv  15696  mulgneg2  15756  oppgmnd  15971  oddvdsnn0  16151  oddvds  16154  odmulg  16161  odcl2  16170  lsmcomx  16442  srgrmhm  16740  rngcom  16779  mulgass2  16798  opprrng  16829  irredrmul  16905  irredlmul  16906  isdrngrd  16964  islmodd  17060  lmodcom  17097  opprdomn  17479  zntoslem  18098  ipcl  18171  maducoevalmin1  18574  rintopn  18638  opnnei  18840  restin  18886  cnpnei  18984  cnprest  19009  ordthaus  19104  kgen2ss  19244  hausflim  19670  fclsfnflim  19716  cnpfcf  19730  opnsubg  19794  cuspcvg  19992  psmetsym  20002  xmetsym  20038  ngpdsr  20312  ngpds2r  20314  ngpds3r  20316  clmmulg  20781  iscau2  20904  dgr1term  21843  cxpeq0  22239  cxpge0  22244  grpoidinvlem2  23827  grpoinvdiv  23867  gxcl  23887  nvpncan  24172  nvsub  24190  nvabs  24196  nvelbl  24219  ipval2lem2  24234  ipval2lem5  24240  dipcj  24247  diporthcom  24249  dipdi  24378  dipassr  24381  dipsubdi  24384  hlipcj  24447  hvadd32  24571  hvsub32  24582  his5  24623  hoadd32  25322  hosubsub  25356  unopf1o  25455  adj2  25473  adjvalval  25476  adjlnop  25625  leopmul2i  25674  cvntr  25831  mdsymlem5  25946  sumdmdii  25954  supxrnemnf  26190  odutos  26258  tlt2  26259  tosglblem  26264  archiabl  26349  unitdivcld  26465  ghomf1olem  27447  gcd32  27691  cgrrflx  28152  cgrcom  28155  cgrcomr  28162  btwntriv1  28181  cgr3com  28218  colineartriv2  28233  segleantisym  28280  seglelin  28281  btwnoutside  28290  ftc1anclem5  28609  clsint2  28662  heibor1  28847  rngoidl  28962  ispridlc  29008  nerabdioph  29285  monotoddzzfi  29421  fzneg  29463  jm2.19lem2  29477  lincvalsng  31057  reccot  31389  sineq0ALT  31973  bnj605  32200  bnj607  32209  opltcon3b  33155  cmtcomlemN  33199  cmtcomN  33200  cmt3N  33202  cmtbr3N  33205  cvrval2  33225  cvrnbtwn4  33230  leatb  33243  atlrelat1  33272  hlatlej2  33326  hlateq  33349  hlrelat5N  33351  snatpsubN  33700  pmap11  33712  paddcom  33763  sspadd2  33766  paddss12  33769  cdleme51finvN  34506  cdleme51finvtrN  34508  cdlemeiota  34535  cdlemg2jlemOLDN  34543  cdlemg2klem  34545  cdlemg4b1  34559  cdlemg4b2  34560  trljco2  34691  tgrpabl  34701  tendoplcom  34732  cdleml6  34931  erngdvlem3-rN  34948  dia11N  34999  dib11N  35111  dih11  35216