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  6005  acexmid  6016  dfsmo2  6452  f1oeng  6929  ctssdc  7311  ltexprlemdisj  7825  ltexprlemfu  7830  recexprlemss1u  7855  mul32  8308  add32  8337  cnegexlem2  8354  subsub23  8383  subadd23  8390  addsub12  8391  subsub  8408  subsub3  8410  sub32  8412  suble  8619  lesub  8620  ltsub23  8621  ltsub13  8622  ltleadd  8625  div32ap  8871  div13ap  8872  div12ap  8873  divdiv32ap  8899  cju  9140  icc0r  10160  fzen  10277  elfz1b  10324  ioo0  10518  ico0  10520  ioc0  10521  expgt0  10833  expge0  10836  expge1  10837  shftval2  11386  abs3dif  11665  divalgb  12485  nnwodc  12606  ctinf  13050  grpinvcnv  13650  mulgaddcom  13732  mulgneg2  13742  srgrmhm  14006  ringcom  14043  mulgass2  14070  opprrng  14089  opprring  14091  unitmulcl  14126  islmodd  14306  lmodcom  14346  rmodislmod  14364  restin  14899  cnpnei  14942  cnptoprest  14962  psmetsym  15052  xmetsym  15091