Theorem 3com12 1207

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  3adant2l  1232  3adant2r  1233  brelrng  4859  iotam  5209  funimaexglem  5300  fvun2  5584  nnaordi  6509  nnmword  6519  fpmg  6674  prcdnql  7483  prcunqu  7484  prarloc  7502  ltaprg  7618  mul12  8086  add12  8115  addsub  8168  addsubeq4  8172  ppncan  8199  leadd1  8387  ltaddsub2  8394  leaddsub2  8396  lemul1  8550  reapmul1lem  8551  reapadd1  8553  reapcotr  8555  remulext1  8556  div23ap  8648  ltmulgt11  8821  lediv1  8826  lemuldiv  8838  zdiv  9341  iooneg  9988  icoshft  9990  fzaddel  10059  fzshftral  10108  facwordi  10720  abssubge0  11111  climshftlemg  11310  dvdsmul1  11820  divalgb  11930  lcmgcdeq  12083  pcfac  12348  mhmmulg  13024  rmodislmodlem  13440  cnmptcom  13801  hmeof1o2  13811