Theorem 3com23 1236

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  3coml  1237  syld3an2  1321  3anidm13  1333  eqreu  3012  f1ofveu  6047  acexmid  6058  dfsmo2  6532  f1oeng  7010  ctssdc  7418  ltexprlemdisj  7938  ltexprlemfu  7943  recexprlemss1u  7968  mul32  8421  add32  8450  cnegexlem2  8467  subsub23  8496  subadd23  8503  addsub12  8504  subsub  8521  subsub3  8523  sub32  8525  suble  8733  lesub  8734  ltsub23  8735  ltsub13  8736  ltleadd  8739  div32ap  8987  div13ap  8988  div12ap  8989  divdiv32ap  9015  cju  9256  icc0r  10282  fzen  10401  elfz1b  10450  ioo0  10647  ico0  10649  ioc0  10650  expgt0  10962  expge0  10965  expge1  10966  shftval2  11540  abs3dif  11820  divalgb  12641  nnwodc  12762  ctinf  13270  grpinvcnv  13828  mulgaddcom  13904  mulgneg2  13914  srgrmhm  14242  ringcom  14279  mulgass2  14306  opprrng  14325  opprring  14327  unitmulcl  14363  islmodd  14572  lmodcom  14612  rmodislmod  14630  restin  15172  cnpnei  15215  cnptoprest  15235  psmetsym  15325  xmetsym  15364