Theorem 3com12 1185

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

Syntax hints:   → wi 4   ∧ w3a 962

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 964

This theorem is referenced by:  3adant2l  1210  3adant2r  1211  brelrng  4770  funimaexglem  5206  fvun2  5488  nnaordi  6404  nnmword  6414  fpmg  6568  prcdnql  7292  prcunqu  7293  prarloc  7311  ltaprg  7427  mul12  7891  add12  7920  addsub  7973  addsubeq4  7977  ppncan  8004  leadd1  8192  ltaddsub2  8199  leaddsub2  8201  lemul1  8355  reapmul1lem  8356  reapadd1  8358  reapcotr  8360  remulext1  8361  div23ap  8451  ltmulgt11  8622  lediv1  8627  lemuldiv  8639  zdiv  9139  iooneg  9771  icoshft  9773  fzaddel  9839  fzshftral  9888  facwordi  10486  abssubge0  10874  climshftlemg  11071  dvdsmul1  11515  divalgb  11622  lcmgcdeq  11764  cnmptcom  12467  hmeof1o2  12477