Theorem 3com23 1235

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

Syntax hints:   → wi 4   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  3coml  1236  syld3an2  1320  3anidm13  1332  eqreu  2998  f1ofveu  6006  acexmid  6017  dfsmo2  6453  f1oeng  6930  ctssdc  7312  ltexprlemdisj  7826  ltexprlemfu  7831  recexprlemss1u  7856  mul32  8309  add32  8338  cnegexlem2  8355  subsub23  8384  subadd23  8391  addsub12  8392  subsub  8409  subsub3  8411  sub32  8413  suble  8620  lesub  8621  ltsub23  8622  ltsub13  8623  ltleadd  8626  div32ap  8872  div13ap  8873  div12ap  8874  divdiv32ap  8900  cju  9141  icc0r  10161  fzen  10278  elfz1b  10325  ioo0  10520  ico0  10522  ioc0  10523  expgt0  10835  expge0  10838  expge1  10839  shftval2  11391  abs3dif  11670  divalgb  12491  nnwodc  12612  ctinf  13056  grpinvcnv  13656  mulgaddcom  13738  mulgneg2  13748  srgrmhm  14013  ringcom  14050  mulgass2  14077  opprrng  14096  opprring  14098  unitmulcl  14133  islmodd  14313  lmodcom  14353  rmodislmod  14371  restin  14906  cnpnei  14949  cnptoprest  14969  psmetsym  15059  xmetsym  15098