Theorem 3com12 1186

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

Syntax hints:   → wi 4   ∧ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3adant2l  1211  3adant2r  1212  brelrng  4778  funimaexglem  5214  fvun2  5496  nnaordi  6412  nnmword  6422  fpmg  6576  prcdnql  7316  prcunqu  7317  prarloc  7335  ltaprg  7451  mul12  7915  add12  7944  addsub  7997  addsubeq4  8001  ppncan  8028  leadd1  8216  ltaddsub2  8223  leaddsub2  8225  lemul1  8379  reapmul1lem  8380  reapadd1  8382  reapcotr  8384  remulext1  8385  div23ap  8475  ltmulgt11  8646  lediv1  8651  lemuldiv  8663  zdiv  9163  iooneg  9801  icoshft  9803  fzaddel  9870  fzshftral  9919  facwordi  10518  abssubge0  10906  climshftlemg  11103  dvdsmul1  11551  divalgb  11658  lcmgcdeq  11800  cnmptcom  12506  hmeof1o2  12516