Theorem 3com23 1110

Description: Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com23	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Proof of Theorem 3com23

Step	Hyp	Ref	Expression
1		3exp.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1103	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 72	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	3imp 1098	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  3coml  1111  syld3an2  1182  3anidm13  1193  eqreu  2733  f1ofveu  5500  acexmid  5511  dfsmo2  5902  f1oeng  6237  ltexprlemdisj  6704  ltexprlemfu  6709  recexprlemss1u  6734  mul32  7143  add32  7170  cnegexlem2  7187  subsub23  7216  subadd23  7223  addsub12  7224  subsub  7241  subsub3  7243  sub32  7245  suble  7435  lesub  7436  ltsub23  7437  ltsub13  7438  ltleadd  7441  div32ap  7671  div13ap  7672  div12ap  7673  divdiv32ap  7696  cju  7913  icc0r  8795  fzen  8907  elfz1b  8952  elfzmlbmOLD  8989  expival  9257  expgt0  9288  expge0  9291  expge1  9292  shftval2  9427  abs3dif  9701