Theorem 3com23 1211

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3coml  1212  syld3an2  1296  3anidm13  1307  eqreu  2953  f1ofveu  5907  acexmid  5918  dfsmo2  6342  f1oeng  6813  ctssdc  7174  ltexprlemdisj  7668  ltexprlemfu  7673  recexprlemss1u  7698  mul32  8151  add32  8180  cnegexlem2  8197  subsub23  8226  subadd23  8233  addsub12  8234  subsub  8251  subsub3  8253  sub32  8255  suble  8461  lesub  8462  ltsub23  8463  ltsub13  8464  ltleadd  8467  div32ap  8713  div13ap  8714  div12ap  8715  divdiv32ap  8741  cju  8982  icc0r  9995  fzen  10112  elfz1b  10159  ioo0  10331  ico0  10333  ioc0  10334  expgt0  10646  expge0  10649  expge1  10650  shftval2  10973  abs3dif  11252  divalgb  12069  nnwodc  12176  ctinf  12590  grpinvcnv  13143  mulgaddcom  13219  mulgneg2  13229  srgrmhm  13493  ringcom  13530  mulgass2  13557  opprrng  13576  opprring  13578  unitmulcl  13612  islmodd  13792  lmodcom  13832  rmodislmod  13850  restin  14355  cnpnei  14398  cnptoprest  14418  psmetsym  14508  xmetsym  14547