Theorem 3com12 1147

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 931	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 119	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 924

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 926

This theorem is referenced by:  3adant2l  1168  3adant2r  1169  brelrng  4666  funimaexglem  5097  fvun2  5371  nnaordi  6267  nnmword  6277  fpmg  6431  prcdnql  7043  prcunqu  7044  prarloc  7062  ltaprg  7178  mul12  7611  add12  7640  addsub  7693  addsubeq4  7697  ppncan  7724  leadd1  7908  ltaddsub2  7915  leaddsub2  7917  lemul1  8070  reapmul1lem  8071  reapadd1  8073  reapcotr  8075  remulext1  8076  div23ap  8158  ltmulgt11  8325  lediv1  8330  lemuldiv  8342  zdiv  8834  iooneg  9405  icoshft  9407  fzaddel  9473  fzshftral  9522  facwordi  10148  abssubge0  10535  climshftlemg  10690  dvdsmul1  11096  divalgb  11203  lcmgcdeq  11343