Theorem 3com12 1123

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  3comr  1125  3com23  1126  brelrng  5908  fnunres2  6634  fresaunres1  6736  fvun2  6956  onfununi  8313  oaword  8516  nnaword  8594  nnmword  8600  naddel1  8654  naddss1  8656  ecopovtrn  8796  fpmg  8844  tskord  10740  ltadd2  11285  mul12  11346  add12  11399  addsub  11439  addsubeq4  11443  ppncan  11471  leadd1  11653  ltaddsub2  11660  leaddsub2  11662  ltsub1  11681  ltsub2  11682  div23  11863  ltmul1  12039  ltmulgt11  12049  lediv1  12055  lemuldiv  12070  ltdiv2  12076  zdiv  12611  xltadd1  13223  xltmul1  13259  iooneg  13439  icoshft  13441  fzaddel  13526  fzshftral  13583  modmulmodr  13909  facwordi  14261  pfxeq  14668  abssubge0  15301  climshftlem  15547  dvdsmul1  16254  divalglem8  16377  divalgb  16381  rprpwr  16536  lcmgcdeq  16589  pcfac  16877  mhmmulg  19054  rmodislmodlem  20842  xrsdsreval  21335  cnmptcom  23572  hmeof1o2  23657  ordthmeo  23696  isclmi0  25005  iscvsi  25036  cxplt2  26614  sleadd1im  27901  sltadd2  27905  addscan2  27907  axcontlem8  28905  vcdi  30501  isvciOLD  30516  dipdi  30779  dipsubdi  30785  hvadd12  30971  hvmulcom  30979  his5  31022  bcs3  31119  chj12  31470  spansnmul  31500  homul12  31741  hoaddsub  31752  lnopmul  31903  lnopaddmuli  31909  lnopsubmuli  31911  lnfnaddmuli  31981  leop2  32060  dmdsl3  32251  chirredlem3  32328  atmd2  32336  cdj3lem3  32374  signstfvc  34572  3com12d  36305  cnambfre  37669  sdclem2  37743  indstrd  42188  addrcom  44471  uun123p1  44805  sineq0ALT  44933  stoweidlem17  46022  sigaras  46860  sigarms  46861  i0oii  48912