Theorem 3com23 1193

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 1186	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	com23 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
4	3	3imp 1181	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  1194  syld3an2  1265  3anidm13  1276  eqreu  3146  f1ofveu  6081  curry2f  6663  dfsmo2  6800  nneob  7083  f1oeng  7320  suppr  7710  infdif  8370  axdclem2  8681  gchen1  8784  grumap  8967  grudomon  8976  mul32  9528  add32  9575  subsub23  9607  subadd23  9614  addsub12  9615  subsub  9631  subsub3  9633  sub32  9635  suble  9809  lesub  9810  ltsub23  9811  ltsub13  9812  ltleadd  9814  div32  10006  div13  10007  div12  10008  divdiv32  10031  cju  10310  infmssuzle  10929  ioo0  11317  ico0  11338  ioc0  11339  icc0  11340  fzen  11459  elfzmlbm  11482  elfz1b  11519  modcyc  11735  expgt0  11889  expge0  11892  expge1  11893  2cshwcom  12442  shftval2  12556  abs3dif  12811  divalgb  13600  submrc  14558  mrieqv2d  14569  pltnlt  15130  pltn2lp  15131  tosso  15198  latnle  15247  latabs1  15249  lubel  15284  ipopos  15322  grpinvcnv  15585  mulgneg2  15645  oppgmnd  15860  oddvdsnn0  16038  oddvds  16041  odmulg  16048  odcl2  16057  lsmcomx  16329  srgrmhm  16625  rngcom  16663  mulgass2  16682  opprrng  16713  irredrmul  16789  irredlmul  16790  isdrngrd  16838  islmodd  16934  lmodcom  16971  opprdomn  17353  zntoslem  17969  ipcl  18042  maducoevalmin1  18438  rintopn  18502  opnnei  18704  restin  18750  cnpnei  18848  cnprest  18873  ordthaus  18968  kgen2ss  19108  hausflim  19534  fclsfnflim  19580  cnpfcf  19594  opnsubg  19658  cuspcvg  19856  psmetsym  19866  xmetsym  19902  ngpdsr  20176  ngpds2r  20178  ngpds3r  20180  clmmulg  20645  iscau2  20768  dgr1term  21707  cxpeq0  22103  cxpge0  22108  grpoidinvlem2  23660  grpoinvdiv  23700  gxcl  23720  nvpncan  24005  nvsub  24023  nvabs  24029  nvelbl  24052  ipval2lem2  24067  ipval2lem5  24073  dipcj  24080  diporthcom  24082  dipdi  24211  dipassr  24214  dipsubdi  24217  hlipcj  24280  hvadd32  24404  hvsub32  24415  his5  24456  hoadd32  25155  hosubsub  25189  unopf1o  25288  adj2  25306  adjvalval  25309  adjlnop  25458  leopmul2i  25507  cvntr  25664  mdsymlem5  25779  sumdmdii  25787  supxrnemnf  26024  odutos  26092  tlt2  26093  tosglblem  26098  archiabl  26183  unitdivcld  26300  ghomf1olem  27282  gcd32  27526  cgrrflx  27987  cgrcom  27990  cgrcomr  27997  btwntriv1  28016  cgr3com  28053  colineartriv2  28068  segleantisym  28115  seglelin  28116  btwnoutside  28125  ftc1anclem5  28442  clsint2  28495  heibor1  28680  rngoidl  28795  ispridlc  28841  nerabdioph  29118  monotoddzzfi  29254  fzneg  29296  jm2.19lem2  29310  lincvalsng  30881  reccot  31024  sineq0ALT  31602  bnj605  31829  bnj607  31838  opltcon3b  32742  cmtcomlemN  32786  cmtcomN  32787  cmt3N  32789  cmtbr3N  32792  cvrval2  32812  cvrnbtwn4  32817  leatb  32830  atlrelat1  32859  hlatlej2  32913  hlateq  32936  hlrelat5N  32938  snatpsubN  33287  pmap11  33299  paddcom  33350  sspadd2  33353  paddss12  33356  cdleme51finvN  34093  cdleme51finvtrN  34095  cdlemeiota  34122  cdlemg2jlemOLDN  34130  cdlemg2klem  34132  cdlemg4b1  34146  cdlemg4b2  34147  trljco2  34278  tgrpabl  34288  tendoplcom  34319  cdleml6  34518  erngdvlem3-rN  34535  dia11N  34586  dib11N  34698  dih11  34803