Theorem 3com23 1211

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

Syntax hints:   -> wi 4   /\ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3coml  1212  syld3an2  1296  3anidm13  1307  eqreu  2956  f1ofveu  5913  acexmid  5924  dfsmo2  6354  f1oeng  6825  ctssdc  7188  ltexprlemdisj  7690  ltexprlemfu  7695  recexprlemss1u  7720  mul32  8173  add32  8202  cnegexlem2  8219  subsub23  8248  subadd23  8255  addsub12  8256  subsub  8273  subsub3  8275  sub32  8277  suble  8484  lesub  8485  ltsub23  8486  ltsub13  8487  ltleadd  8490  div32ap  8736  div13ap  8737  div12ap  8738  divdiv32ap  8764  cju  9005  icc0r  10018  fzen  10135  elfz1b  10182  ioo0  10366  ico0  10368  ioc0  10369  expgt0  10681  expge0  10684  expge1  10685  shftval2  11008  abs3dif  11287  divalgb  12107  nnwodc  12228  ctinf  12672  grpinvcnv  13270  mulgaddcom  13352  mulgneg2  13362  srgrmhm  13626  ringcom  13663  mulgass2  13690  opprrng  13709  opprring  13711  unitmulcl  13745  islmodd  13925  lmodcom  13965  rmodislmod  13983  restin  14496  cnpnei  14539  cnptoprest  14559  psmetsym  14649  xmetsym  14688