Theorem 3com12 1234

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 1012	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 121	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:  3adant2l  1259  3adant2r  1260  brelrng  4993  iotam  5349  funimaexglem  5444  fresaunres1disj  5551  fvun2  5749  nnaordi  6754  nnmword  6764  fpmg  6921  prcdnql  7815  prcunqu  7816  prarloc  7834  ltaprg  7950  mul12  8418  add12  8447  addsub  8500  addsubeq4  8504  ppncan  8531  leadd1  8721  ltaddsub2  8728  leaddsub2  8730  lemul1  8884  reapmul1lem  8885  reapadd1  8887  reapcotr  8889  remulext1  8890  div23ap  8982  ltmulgt11  9155  lediv1  9160  lemuldiv  9172  zdiv  9684  iooneg  10340  icoshft  10342  fzaddel  10414  fzshftral  10464  facwordi  11127  pfxeq  11413  abssubge0  11812  climshftlemg  12012  dvdsmul1  12524  divalgb  12636  lcmgcdeq  12805  pcfac  13073  mhmmulg  13916  rmodislmodlem  14624  cnmptcom  15289  hmeof1o2  15299