Theorem 3com12 1139

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 1135	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp21 1129	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  3comr  1141  3com23  1142  brelrng  5929  fnunres2  6646  fresaunres1  6749  fvun2  6971  onfununi  8324  oaword  8530  nnaword  8609  nnmword  8615  naddel1  8670  naddss1  8672  ecopovtrn  8814  fpmg  8862  tskord  10761  ltadd2  11310  mul12  11371  add12  11424  addsub  11464  addsubeq4  11468  ppncan  11496  leadd1  11678  ltaddsub2  11685  leaddsub2  11687  ltsub1  11706  ltsub2  11707  div23  11887  ltmul1  12061  ltmulgt11  12070  lediv1  12076  lemuldiv  12091  ltdiv2  12097  zdiv  12662  xltadd1  13278  xltmul1  13314  iooneg  13494  icoshft  13496  fzaddel  13582  fzshftral  13639  modmulmodr  13969  facwordi  14321  pfxeq  14729  abssubge0  15375  climshftlem  15621  dvdsmul1  16331  divalglem8  16454  divalgb  16458  rprpwr  16613  lcmgcdeq  16666  pcfac  16955  mhmmulg  19177  rmodislmodlem  21024  xrsdsreval  21527  cnmptcom  23800  hmeof1o2  23885  ordthmeo  23924  isclmi0  25222  iscvsi  25253  cxplt2  26825  leadds1im  28142  ltadds2  28146  addscan2  28148  axcontlem8  29258  vcdi  30854  isvciOLD  30869  dipdi  31132  dipsubdi  31138  hvadd12  31324  hvmulcom  31332  his5  31375  bcs3  31472  chj12  31823  spansnmul  31853  homul12  32094  hoaddsub  32105  lnopmul  32256  lnopaddmuli  32262  lnopsubmuli  32264  lnfnaddmuli  32334  leop2  32413  dmdsl3  32604  chirredlem3  32681  atmd2  32689  cdj3lem3  32727  signstfvc  34902  3com12d  36707  cnambfre  38202  sdclem2  38276  indstrd  42845  addrcom  45068  uun123p1  45402  sineq0ALT  45530  stoweidlem17  46616  sigaras  47454  sigarms  47455  i0oii  49576