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  5883  fresaunres1  6699  fvun2  6917  onfununi  8243  oaword  8452  nnaword  8530  nnmword  8536  ecopovtrn  8681  fpmg  8728  tskord  10638  ltadd2  11181  mul12  11242  add12  11294  addsub  11334  addsubeq4  11338  ppncan  11365  leadd1  11545  ltaddsub2  11552  leaddsub2  11554  ltsub1  11573  ltsub2  11574  div23  11754  ltmul1  11927  ltmulgt11  11937  lediv1  11942  lemuldiv  11957  ltdiv2  11963  zdiv  12492  xltadd1  13092  xltmul1  13128  iooneg  13305  icoshft  13307  fzaddel  13392  fzshftral  13446  modmulmodr  13759  facwordi  14105  pfxeq  14508  abssubge0  15139  climshftlem  15383  dvdsmul1  16087  divalglem8  16209  divalgb  16213  rprpwr  16366  lcmgcdeq  16415  pcfac  16698  mhmmulg  18841  rmodislmodlem  20297  xrsdsreval  20750  cnmptcom  22936  hmeof1o2  23021  ordthmeo  23060  isclmi0  24368  iscvsi  24399  cxplt2  25960  axcontlem8  27629  vcdi  29216  isvciOLD  29231  dipdi  29494  dipsubdi  29500  hvadd12  29686  hvmulcom  29694  his5  29737  bcs3  29834  chj12  30185  spansnmul  30215  homul12  30456  hoaddsub  30467  lnopmul  30618  lnopaddmuli  30624  lnopsubmuli  30626  lnfnaddmuli  30696  leop2  30775  dmdsl3  30966  chirredlem3  31043  atmd2  31051  cdj3lem3  31089  signstfvc  32853  naddel1  34126  naddss1  34128  sleadd1im  34250  sltadd2  34254  addscan2  34256  3com12d  34638  cnambfre  35981  sdclem2  36056  addrcom  42466  uun123p1  42802  sineq0ALT  42930  stoweidlem17  43946  sigaras  44774  sigarms  44775  i0oii  46631