Theorem 3com12 1260

Description: Commutation in antecedent. Swap 1st and 2nd. (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 1037	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜑 ∧ 𝜓 ∧ 𝜒))
2		3exp.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 205	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 195  df-an 384  df-3an 1032

This theorem is referenced by:  3imp21  1268  3adant2l  1311  3adant2r  1312  brelrng  5263  fresaunres1  5975  fvun2  6165  onfununi  7302  oaword  7493  nnaword  7571  nnmword  7577  ecopovtrn  7714  fpmg  7746  tskord  9458  ltadd2  9992  mul12  10053  add12  10104  addsub  10143  addsubeq4  10147  ppncan  10174  leadd1  10345  ltaddsub2  10352  leaddsub2  10354  ltsub1  10373  ltsub2  10374  div23  10553  ltmul1  10722  ltmulgt11  10732  lediv1  10737  lemuldiv  10752  ltdiv2  10758  zdiv  11279  xltadd1  11915  xltmul1  11951  iooneg  12119  icoshft  12121  fzaddel  12201  fzshftral  12252  modmulmodr  12553  facwordi  12893  abssubge0  13861  climshftlem  14099  dvdsmul1  14787  divalglem8  14907  divalgb  14911  lcmgcdeq  15109  pcfac  15387  mhmmulg  17352  xrsdsreval  19556  cnmptcom  21233  hmeof1o2  21318  ordthmeo  21357  isclmi0  22637  iscvsi  22666  cxplt2  24161  axcontlem8  25569  clwwlkndivn  26130  vcdi  26573  isvciOLD  26603  dipdi  26888  dipsubdi  26894  hvadd12  27082  hvmulcom  27090  his5  27133  bcs3  27230  chj12  27583  spansnmul  27613  homul12  27854  hoaddsub  27865  lnopmul  28016  lnopaddmuli  28022  lnopsubmuli  28024  lnfnaddmuli  28094  leop2  28173  dmdsl3  28364  chirredlem3  28441  atmd2  28449  cdj3lem3  28487  signstfvc  29783  3com12d  31280  cnambfre  32431  sdclem2  32511  addrcom  37503  uun123p1  37860  sineq0ALT  37998  stoweidlem17  38714  sigaras  39497  sigarms  39498