Theorem 3com23 1191

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

Syntax hints:   -> wi 4   /\ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3coml  1192  syld3an2  1267  3anidm13  1278  eqreu  2904  f1ofveu  5809  acexmid  5820  dfsmo2  6231  f1oeng  6699  ctssdc  7051  ltexprlemdisj  7520  ltexprlemfu  7525  recexprlemss1u  7550  mul32  7999  add32  8028  cnegexlem2  8045  subsub23  8074  subadd23  8081  addsub12  8082  subsub  8099  subsub3  8101  sub32  8103  suble  8309  lesub  8310  ltsub23  8311  ltsub13  8312  ltleadd  8315  div32ap  8559  div13ap  8560  div12ap  8561  divdiv32ap  8587  cju  8826  icc0r  9823  fzen  9938  elfz1b  9985  ioo0  10152  ico0  10154  ioc0  10155  expgt0  10445  expge0  10448  expge1  10449  shftval2  10719  abs3dif  10998  divalgb  11808  ctinf  12142  restin  12547  cnpnei  12590  cnptoprest  12610  psmetsym  12700  xmetsym  12739