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  4994  iotam  5350  funimaexglem  5445  fresaunres1disj  5552  fvun2  5750  nnaordi  6755  nnmword  6765  fpmg  6922  prcdnql  7816  prcunqu  7817  prarloc  7835  ltaprg  7951  mul12  8420  add12  8449  addsub  8502  addsubeq4  8506  ppncan  8533  leadd1  8723  ltaddsub2  8730  leaddsub2  8732  lemul1  8886  reapmul1lem  8887  reapadd1  8889  reapcotr  8891  remulext1  8892  div23ap  8986  ltmulgt11  9159  lediv1  9164  lemuldiv  9176  zdiv  9688  iooneg  10344  icoshft  10346  fzaddel  10418  fzshftral  10468  facwordi  11131  pfxeq  11417  abssubge0  11817  climshftlemg  12017  dvdsmul1  12529  divalgb  12641  lcmgcdeq  12810  pcfac  13078  mhmmulg  13921  rmodislmodlem  14629  cnmptcom  15294  hmeof1o2  15304