Theorem 3com12 1129

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3comr  1131  3com23  1132  brelrng  5890  fnunres2  6605  fresaunres1  6707  fvun2  6926  onfununi  8278  oaword  8481  nnaword  8560  nnmword  8566  naddel1  8620  naddss1  8622  ecopovtrn  8764  fpmg  8813  tskord  10701  ltadd2  11248  mul12  11309  add12  11362  addsub  11402  addsubeq4  11406  ppncan  11434  leadd1  11616  ltaddsub2  11623  leaddsub2  11625  ltsub1  11644  ltsub2  11645  div23  11826  ltmul1  12003  ltmulgt11  12013  lediv1  12019  lemuldiv  12034  ltdiv2  12040  zdiv  12597  xltadd1  13206  xltmul1  13242  iooneg  13422  icoshft  13424  fzaddel  13510  fzshftral  13567  modmulmodr  13897  facwordi  14249  pfxeq  14656  abssubge0  15288  climshftlem  15534  dvdsmul1  16244  divalglem8  16367  divalgb  16371  rprpwr  16526  lcmgcdeq  16579  pcfac  16868  mhmmulg  19089  rmodislmodlem  20926  xrsdsreval  21394  cnmptcom  23668  hmeof1o2  23753  ordthmeo  23792  isclmi0  25090  iscvsi  25121  cxplt2  26687  leadds1im  28004  ltadds2  28008  addscan2  28010  axcontlem8  29065  vcdi  30661  isvciOLD  30676  dipdi  30939  dipsubdi  30945  hvadd12  31131  hvmulcom  31139  his5  31182  bcs3  31279  chj12  31630  spansnmul  31660  homul12  31901  hoaddsub  31912  lnopmul  32063  lnopaddmuli  32069  lnopsubmuli  32071  lnfnaddmuli  32141  leop2  32220  dmdsl3  32411  chirredlem3  32488  atmd2  32496  cdj3lem3  32534  signstfvc  34765  3com12d  36545  cnambfre  38042  sdclem2  38116  indstrd  42685  addrcom  44925  uun123p1  45259  sineq0ALT  45387  stoweidlem17  46467  sigaras  47305  sigarms  47306  i0oii  49417