Theorem 3com12 1124

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3comr  1126  3com23  1127  brelrng  5898  fnunres2  6613  fresaunres1  6715  fvun2  6934  onfununi  8283  oaword  8486  nnaword  8565  nnmword  8571  naddel1  8625  naddss1  8627  ecopovtrn  8769  fpmg  8818  tskord  10703  ltadd2  11249  mul12  11310  add12  11363  addsub  11403  addsubeq4  11407  ppncan  11435  leadd1  11617  ltaddsub2  11624  leaddsub2  11626  ltsub1  11645  ltsub2  11646  div23  11827  ltmul1  12003  ltmulgt11  12013  lediv1  12019  lemuldiv  12034  ltdiv2  12040  zdiv  12574  xltadd1  13183  xltmul1  13219  iooneg  13399  icoshft  13401  fzaddel  13486  fzshftral  13543  modmulmodr  13872  facwordi  14224  pfxeq  14631  abssubge0  15263  climshftlem  15509  dvdsmul1  16216  divalglem8  16339  divalgb  16343  rprpwr  16498  lcmgcdeq  16551  pcfac  16839  mhmmulg  19057  rmodislmodlem  20892  xrsdsreval  21378  cnmptcom  23634  hmeof1o2  23719  ordthmeo  23758  isclmi0  25066  iscvsi  25097  cxplt2  26675  leadds1im  27995  ltadds2  27999  addscan2  28001  axcontlem8  29056  vcdi  30652  isvciOLD  30667  dipdi  30930  dipsubdi  30936  hvadd12  31122  hvmulcom  31130  his5  31173  bcs3  31270  chj12  31621  spansnmul  31651  homul12  31892  hoaddsub  31903  lnopmul  32054  lnopaddmuli  32060  lnopsubmuli  32062  lnfnaddmuli  32132  leop2  32211  dmdsl3  32402  chirredlem3  32479  atmd2  32487  cdj3lem3  32525  signstfvc  34751  3com12d  36523  cnambfre  37916  sdclem2  37990  indstrd  42560  addrcom  44827  uun123p1  45161  sineq0ALT  45289  stoweidlem17  46372  sigaras  47210  sigarms  47211  i0oii  49276