Theorem 3com23 1188

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

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  1189  syld3an2  1264  3anidm13  1275  eqreu  2880  f1ofveu  5770  acexmid  5781  dfsmo2  6192  f1oeng  6659  ctssdc  7006  ltexprlemdisj  7438  ltexprlemfu  7443  recexprlemss1u  7468  mul32  7916  add32  7945  cnegexlem2  7962  subsub23  7991  subadd23  7998  addsub12  7999  subsub  8016  subsub3  8018  sub32  8020  suble  8226  lesub  8227  ltsub23  8228  ltsub13  8229  ltleadd  8232  div32ap  8476  div13ap  8477  div12ap  8478  divdiv32ap  8504  cju  8743  icc0r  9739  fzen  9854  elfz1b  9901  ioo0  10068  ico0  10070  ioc0  10071  expgt0  10357  expge0  10360  expge1  10361  shftval2  10630  abs3dif  10909  divalgb  11658  ctinf  11979  restin  12384  cnpnei  12427  cnptoprest  12447  psmetsym  12537  xmetsym  12576