Theorem 3com23 1144

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 1137	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	com23 77	. 2 ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃)))
4	3	3imp 1132	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3coml  1145  syld3an2  1216  3anidm13  1227  eqreu  2784  f1ofveu  5520  acexmid  5531  dfsmo2  5925  f1oeng  6260  ltexprlemdisj  6796  ltexprlemfu  6801  recexprlemss1u  6826  mul32  7238  add32  7267  cnegexlem2  7284  subsub23  7313  subadd23  7320  addsub12  7321  subsub  7338  subsub3  7340  sub32  7342  suble  7544  lesub  7545  ltsub23  7546  ltsub13  7547  ltleadd  7550  div32ap  7780  div13ap  7781  div12ap  7782  divdiv32ap  7808  cju  8038  icc0r  8949  fzen  9062  elfz1b  9107  ioo0  9268  ico0  9270  ioc0  9271  expival  9478  expgt0  9509  expge0  9512  expge1  9513  shftval2  9714  abs3dif  9991  divalgb  10325