Theorem 3com12 1209

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  3adant2l  1234  3adant2r  1235  brelrng  4898  iotam  5251  funimaexglem  5342  fvun2  5631  nnaordi  6575  nnmword  6585  fpmg  6742  prcdnql  7570  prcunqu  7571  prarloc  7589  ltaprg  7705  mul12  8174  add12  8203  addsub  8256  addsubeq4  8260  ppncan  8287  leadd1  8476  ltaddsub2  8483  leaddsub2  8485  lemul1  8639  reapmul1lem  8640  reapadd1  8642  reapcotr  8644  remulext1  8645  div23ap  8737  ltmulgt11  8910  lediv1  8915  lemuldiv  8927  zdiv  9433  iooneg  10082  icoshft  10084  fzaddel  10153  fzshftral  10202  facwordi  10851  abssubge0  11286  climshftlemg  11486  dvdsmul1  11997  divalgb  12109  lcmgcdeq  12278  pcfac  12546  mhmmulg  13371  rmodislmodlem  13984  cnmptcom  14642  hmeof1o2  14652