Theorem 3com12 1207

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  3adant2l  1232  3adant2r  1233  brelrng  4851  iotam  5200  funimaexglem  5291  fvun2  5575  nnaordi  6499  nnmword  6509  fpmg  6664  prcdnql  7458  prcunqu  7459  prarloc  7477  ltaprg  7593  mul12  8060  add12  8089  addsub  8142  addsubeq4  8146  ppncan  8173  leadd1  8361  ltaddsub2  8368  leaddsub2  8370  lemul1  8524  reapmul1lem  8525  reapadd1  8527  reapcotr  8529  remulext1  8530  div23ap  8621  ltmulgt11  8794  lediv1  8799  lemuldiv  8811  zdiv  9314  iooneg  9959  icoshft  9961  fzaddel  10029  fzshftral  10078  facwordi  10688  abssubge0  11079  climshftlemg  11278  dvdsmul1  11788  divalgb  11897  lcmgcdeq  12050  pcfac  12315  mhmmulg  12884  cnmptcom  13369  hmeof1o2  13379