Theorem 3com23 1204

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

Syntax hints:   -> wi 4   /\ w3a 973

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 975

This theorem is referenced by:  3coml  1205  syld3an2  1280  3anidm13  1291  eqreu  2922  f1ofveu  5841  acexmid  5852  dfsmo2  6266  f1oeng  6735  ctssdc  7090  ltexprlemdisj  7568  ltexprlemfu  7573  recexprlemss1u  7598  mul32  8049  add32  8078  cnegexlem2  8095  subsub23  8124  subadd23  8131  addsub12  8132  subsub  8149  subsub3  8151  sub32  8153  suble  8359  lesub  8360  ltsub23  8361  ltsub13  8362  ltleadd  8365  div32ap  8609  div13ap  8610  div12ap  8611  divdiv32ap  8637  cju  8877  icc0r  9883  fzen  9999  elfz1b  10046  ioo0  10216  ico0  10218  ioc0  10219  expgt0  10509  expge0  10512  expge1  10513  shftval2  10790  abs3dif  11069  divalgb  11884  nnwodc  11991  ctinf  12385  grpinvcnv  12767  restin  12970  cnpnei  13013  cnptoprest  13033  psmetsym  13123  xmetsym  13162