Theorem 3com12 1121

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

Syntax hints:   → wi 4   ∧ w3a 1085

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

This theorem is referenced by:  3comr  1123  3com23  1124  brelrng  5839  fresaunres1  6631  fvun2  6842  onfununi  8143  oaword  8342  nnaword  8420  nnmword  8426  ecopovtrn  8567  fpmg  8614  tskord  10467  ltadd2  11009  mul12  11070  add12  11122  addsub  11162  addsubeq4  11166  ppncan  11193  leadd1  11373  ltaddsub2  11380  leaddsub2  11382  ltsub1  11401  ltsub2  11402  div23  11582  ltmul1  11755  ltmulgt11  11765  lediv1  11770  lemuldiv  11785  ltdiv2  11791  zdiv  12320  xltadd1  12919  xltmul1  12955  iooneg  13132  icoshft  13134  fzaddel  13219  fzshftral  13273  modmulmodr  13585  facwordi  13931  pfxeq  14337  abssubge0  14967  climshftlem  15211  dvdsmul1  15915  divalglem8  16037  divalgb  16041  rprpwr  16196  lcmgcdeq  16245  pcfac  16528  mhmmulg  18659  rmodislmodlem  20105  xrsdsreval  20555  cnmptcom  22737  hmeof1o2  22822  ordthmeo  22861  isclmi0  24167  iscvsi  24198  cxplt2  25758  axcontlem8  27242  vcdi  28828  isvciOLD  28843  dipdi  29106  dipsubdi  29112  hvadd12  29298  hvmulcom  29306  his5  29349  bcs3  29446  chj12  29797  spansnmul  29827  homul12  30068  hoaddsub  30079  lnopmul  30230  lnopaddmuli  30236  lnopsubmuli  30238  lnfnaddmuli  30308  leop2  30387  dmdsl3  30578  chirredlem3  30655  atmd2  30663  cdj3lem3  30701  signstfvc  32453  naddel1  33766  naddss1  33768  3com12d  34426  cnambfre  35752  sdclem2  35827  addrcom  41982  uun123p1  42318  sineq0ALT  42446  stoweidlem17  43448  sigaras  44258  sigarms  44259  i0oii  46101