Theorem 3com12 1261

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

Syntax hints:   → wi 4   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3imp21  1269  3adant2l  1312  3adant2r  1313  brelrng  5276  fresaunres1  5990  fvun2  6180  onfununi  7325  oaword  7516  nnaword  7594  nnmword  7600  ecopovtrn  7737  fpmg  7769  tskord  9481  ltadd2  10020  mul12  10081  add12  10132  addsub  10171  addsubeq4  10175  ppncan  10202  leadd1  10375  ltaddsub2  10382  leaddsub2  10384  ltsub1  10403  ltsub2  10404  div23  10583  ltmul1  10752  ltmulgt11  10762  lediv1  10767  lemuldiv  10782  ltdiv2  10788  zdiv  11323  xltadd1  11958  xltmul1  11994  iooneg  12163  icoshft  12165  fzaddel  12246  fzshftral  12297  modmulmodr  12598  facwordi  12938  abssubge0  13915  climshftlem  14153  dvdsmul1  14841  divalglem8  14961  divalgb  14965  lcmgcdeq  15163  pcfac  15441  mhmmulg  17406  xrsdsreval  19610  cnmptcom  21291  hmeof1o2  21376  ordthmeo  21415  isclmi0  22706  iscvsi  22737  cxplt2  24244  axcontlem8  25651  clwwlkndivn  26364  vcdi  26804  isvciOLD  26819  dipdi  27082  dipsubdi  27088  hvadd12  27276  hvmulcom  27284  his5  27327  bcs3  27424  chj12  27777  spansnmul  27807  homul12  28048  hoaddsub  28059  lnopmul  28210  lnopaddmuli  28216  lnopsubmuli  28218  lnfnaddmuli  28288  leop2  28367  dmdsl3  28558  chirredlem3  28635  atmd2  28643  cdj3lem3  28681  signstfvc  29977  3com12d  31474  cnambfre  32628  sdclem2  32708  addrcom  37700  uun123p1  38057  sineq0ALT  38195  stoweidlem17  38910  sigaras  39693  sigarms  39694