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  5894  fnunres2  6613  fresaunres1  6715  fvun2  6935  onfununi  8287  oaword  8490  nnaword  8568  nnmword  8574  naddel1  8628  naddss1  8630  ecopovtrn  8770  fpmg  8818  tskord  10709  ltadd2  11254  mul12  11315  add12  11368  addsub  11408  addsubeq4  11412  ppncan  11440  leadd1  11622  ltaddsub2  11629  leaddsub2  11631  ltsub1  11650  ltsub2  11651  div23  11832  ltmul1  12008  ltmulgt11  12018  lediv1  12024  lemuldiv  12039  ltdiv2  12045  zdiv  12580  xltadd1  13192  xltmul1  13228  iooneg  13408  icoshft  13410  fzaddel  13495  fzshftral  13552  modmulmodr  13878  facwordi  14230  pfxeq  14637  abssubge0  15270  climshftlem  15516  dvdsmul1  16223  divalglem8  16346  divalgb  16350  rprpwr  16505  lcmgcdeq  16558  pcfac  16846  mhmmulg  19023  rmodislmodlem  20811  xrsdsreval  21304  cnmptcom  23541  hmeof1o2  23626  ordthmeo  23665  isclmi0  24974  iscvsi  25005  cxplt2  26583  sleadd1im  27870  sltadd2  27874  addscan2  27876  axcontlem8  28874  vcdi  30467  isvciOLD  30482  dipdi  30745  dipsubdi  30751  hvadd12  30937  hvmulcom  30945  his5  30988  bcs3  31085  chj12  31436  spansnmul  31466  homul12  31707  hoaddsub  31718  lnopmul  31869  lnopaddmuli  31875  lnopsubmuli  31877  lnfnaddmuli  31947  leop2  32026  dmdsl3  32217  chirredlem3  32294  atmd2  32302  cdj3lem3  32340  signstfvc  34538  3com12d  36271  cnambfre  37635  sdclem2  37709  indstrd  42154  addrcom  44437  uun123p1  44771  sineq0ALT  44899  stoweidlem17  45988  sigaras  46826  sigarms  46827  i0oii  48881