Theorem 3com12 1231

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  3adant2l  1256  3adant2r  1257  brelrng  4961  iotam  5316  funimaexglem  5410  fvun2  5709  nnaordi  6671  nnmword  6681  fpmg  6838  prcdnql  7694  prcunqu  7695  prarloc  7713  ltaprg  7829  mul12  8298  add12  8327  addsub  8380  addsubeq4  8384  ppncan  8411  leadd1  8600  ltaddsub2  8607  leaddsub2  8609  lemul1  8763  reapmul1lem  8764  reapadd1  8766  reapcotr  8768  remulext1  8769  div23ap  8861  ltmulgt11  9034  lediv1  9039  lemuldiv  9051  zdiv  9558  iooneg  10213  icoshft  10215  fzaddel  10284  fzshftral  10333  facwordi  10992  pfxeq  11267  abssubge0  11653  climshftlemg  11853  dvdsmul1  12364  divalgb  12476  lcmgcdeq  12645  pcfac  12913  mhmmulg  13740  rmodislmodlem  14354  cnmptcom  15012  hmeof1o2  15022