Theorem 3com12 1120

Description: Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3com12	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem 3com12

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1116	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp21 1111	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3comr  1122  3com23  1123  brelrng  5775  fresaunres1  6525  fvun2  6730  onfununi  7961  oaword  8158  nnaword  8236  nnmword  8242  ecopovtrn  8383  fpmg  8415  tskord  10191  ltadd2  10733  mul12  10794  add12  10846  addsub  10886  addsubeq4  10890  ppncan  10917  leadd1  11097  ltaddsub2  11104  leaddsub2  11106  ltsub1  11125  ltsub2  11126  div23  11306  ltmul1  11479  ltmulgt11  11489  lediv1  11494  lemuldiv  11509  ltdiv2  11515  zdiv  12040  xltadd1  12637  xltmul1  12673  iooneg  12849  icoshft  12851  fzaddel  12936  fzshftral  12990  modmulmodr  13300  facwordi  13645  pfxeq  14049  abssubge0  14679  climshftlem  14923  dvdsmul1  15623  divalglem8  15741  divalgb  15745  lcmgcdeq  15946  pcfac  16225  mhmmulg  18260  rmodislmodlem  19694  xrsdsreval  20136  cnmptcom  22283  hmeof1o2  22368  ordthmeo  22407  isclmi0  23703  iscvsi  23734  cxplt2  25289  axcontlem8  26765  vcdi  28348  isvciOLD  28363  dipdi  28626  dipsubdi  28632  hvadd12  28818  hvmulcom  28826  his5  28869  bcs3  28966  chj12  29317  spansnmul  29347  homul12  29588  hoaddsub  29599  lnopmul  29750  lnopaddmuli  29756  lnopsubmuli  29758  lnfnaddmuli  29828  leop2  29907  dmdsl3  30098  chirredlem3  30175  atmd2  30183  cdj3lem3  30221  signstfvc  31954  3com12d  33771  cnambfre  35105  sdclem2  35180  addrcom  41179  uun123p1  41515  sineq0ALT  41643  stoweidlem17  42659  sigaras  43469  sigarms  43470