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

This theorem is referenced by:  3comr  1124  3com23  1125  brelrng  5955  fnunres2  6682  fresaunres1  6782  fvun2  7001  onfununi  8380  oaword  8586  nnaword  8664  nnmword  8670  naddel1  8724  naddss1  8726  ecopovtrn  8859  fpmg  8907  tskord  10818  ltadd2  11363  mul12  11424  add12  11477  addsub  11517  addsubeq4  11521  ppncan  11549  leadd1  11729  ltaddsub2  11736  leaddsub2  11738  ltsub1  11757  ltsub2  11758  div23  11939  ltmul1  12115  ltmulgt11  12125  lediv1  12131  lemuldiv  12146  ltdiv2  12152  zdiv  12686  xltadd1  13295  xltmul1  13331  iooneg  13508  icoshft  13510  fzaddel  13595  fzshftral  13652  modmulmodr  13975  facwordi  14325  pfxeq  14731  abssubge0  15363  climshftlem  15607  dvdsmul1  16312  divalglem8  16434  divalgb  16438  rprpwr  16593  lcmgcdeq  16646  pcfac  16933  mhmmulg  19146  rmodislmodlem  20944  xrsdsreval  21447  cnmptcom  23702  hmeof1o2  23787  ordthmeo  23826  isclmi0  25145  iscvsi  25176  cxplt2  26755  sleadd1im  28035  sltadd2  28039  addscan2  28041  axcontlem8  29001  vcdi  30594  isvciOLD  30609  dipdi  30872  dipsubdi  30878  hvadd12  31064  hvmulcom  31072  his5  31115  bcs3  31212  chj12  31563  spansnmul  31593  homul12  31834  hoaddsub  31845  lnopmul  31996  lnopaddmuli  32002  lnopsubmuli  32004  lnfnaddmuli  32074  leop2  32153  dmdsl3  32344  chirredlem3  32421  atmd2  32429  cdj3lem3  32467  signstfvc  34568  3com12d  36293  cnambfre  37655  sdclem2  37729  indstrd  42175  addrcom  44471  uun123p1  44807  sineq0ALT  44935  stoweidlem17  45973  sigaras  46811  sigarms  46812  i0oii  48716