Theorem 3com12 1141

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3comr  1143  3com23  1144  brelrng  5922  fnunres2  6653  fresaunres1  6756  fvun2  6978  onfununi  8353  oaword  8561  nnaword  8640  nnmword  8646  naddel1  8701  naddss1  8703  ecopovtrn  8845  fpmg  8900  tskord  10869  ltadd2  11418  mul12  11479  add12  11532  addsub  11572  addsubeq4  11576  ppncan  11604  leadd1  11788  ltaddsub2  11795  leaddsub2  11797  ltsub1  11816  ltsub2  11817  div23  11997  ltmul1  12171  ltmulgt11  12180  lediv1  12186  lemuldiv  12201  ltdiv2  12207  zdiv  12773  xltadd1  13390  xltmul1  13426  iooneg  13606  icoshft  13608  fzaddel  13696  fzshftral  13753  modmulmodr  14084  facwordi  14437  pfxeq  14850  abssubge0  15501  climshftlem  15747  dvdsmul1  16453  divalglem8  16576  divalgb  16580  rprpwr  16739  lcmgcdeq  16793  pcfac  17083  mhmmulg  19331  rmodislmodlem  21210  xrsdsreval  21724  cnmptcom  24003  hmeof1o2  24088  ordthmeo  24127  isclmi0  25425  iscvsi  25456  cxplt2  27032  leadds1im  28379  ltadds2  28383  addscan2  28385  axcontlem8  29555  vcdi  31173  isvciOLD  31188  dipdi  31451  dipsubdi  31457  hvadd12  31643  hvmulcom  31651  his5  31694  bcs3  31791  chj12  32142  spansnmul  32172  homul12  32413  hoaddsub  32424  lnopmul  32575  lnopaddmuli  32581  lnopsubmuli  32583  lnfnaddmuli  32653  leop2  32732  dmdsl3  32923  chirredlem3  33000  atmd2  33008  cdj3lem3  33046  signstfvc  35250  3com12d  37192  cnambfre  38680  sdclem2  38770  indstrd  43337  addrcom  45551  uun123p1  45885  sineq0ALT  46013  stoweidlem17  47121  sigaras  47959  sigarms  47960  i0oii  50128