Theorem 3com12 1143

Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com12	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem 3com12

Step	Hyp	Ref	Expression
1		3ancoma 927	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 119	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 920

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  3adant2l  1164  3adant2r  1165  brelrng  4587  funimaexglem  5007  fvun2  5266  nnaordi  6140  nnmword  6150  prcdnql  6725  prcunqu  6726  prarloc  6744  ltaprg  6860  mul12  7293  add12  7322  addsub  7375  addsubeq4  7379  ppncan  7406  leadd1  7590  ltaddsub2  7597  leaddsub2  7599  lemul1  7749  reapmul1lem  7750  reapadd1  7752  reapcotr  7754  remulext1  7755  div23ap  7835  ltmulgt11  7998  lediv1  8003  lemuldiv  8015  zdiv  8505  iooneg  9075  icoshft  9077  fzaddel  9142  fzshftral  9190  facwordi  9753  abssubge0  10115  climshftlemg  10268  dvdsmul1  10351  divalgb  10458  lcmgcdeq  10598