Theorem 3com12 1122

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 1118	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3comr  1124  3com23  1125  brelrng  5853  fresaunres1  6656  fvun2  6869  onfununi  8181  oaword  8389  nnaword  8467  nnmword  8473  ecopovtrn  8618  fpmg  8665  tskord  10545  ltadd2  11088  mul12  11149  add12  11201  addsub  11241  addsubeq4  11245  ppncan  11272  leadd1  11452  ltaddsub2  11459  leaddsub2  11461  ltsub1  11480  ltsub2  11481  div23  11661  ltmul1  11834  ltmulgt11  11844  lediv1  11849  lemuldiv  11864  ltdiv2  11870  zdiv  12399  xltadd1  12999  xltmul1  13035  iooneg  13212  icoshft  13214  fzaddel  13299  fzshftral  13353  modmulmodr  13666  facwordi  14012  pfxeq  14418  abssubge0  15048  climshftlem  15292  dvdsmul1  15996  divalglem8  16118  divalgb  16122  rprpwr  16277  lcmgcdeq  16326  pcfac  16609  mhmmulg  18753  rmodislmodlem  20199  xrsdsreval  20652  cnmptcom  22838  hmeof1o2  22923  ordthmeo  22962  isclmi0  24270  iscvsi  24301  cxplt2  25862  axcontlem8  27348  vcdi  28936  isvciOLD  28951  dipdi  29214  dipsubdi  29220  hvadd12  29406  hvmulcom  29414  his5  29457  bcs3  29554  chj12  29905  spansnmul  29935  homul12  30176  hoaddsub  30187  lnopmul  30338  lnopaddmuli  30344  lnopsubmuli  30346  lnfnaddmuli  30416  leop2  30495  dmdsl3  30686  chirredlem3  30763  atmd2  30771  cdj3lem3  30809  signstfvc  32562  naddel1  33848  naddss1  33850  3com12d  34508  cnambfre  35834  sdclem2  35909  addrcom  42100  uun123p1  42436  sineq0ALT  42564  stoweidlem17  43565  sigaras  44382  sigarms  44383  i0oii  46224