Theorem 3com12 1141

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3comr  1143  3com23  1144  brelrng  5923  fnunres2  6650  fresaunres1  6753  fvun2  6975  onfununi  8342  oaword  8550  nnaword  8629  nnmword  8635  naddel1  8690  naddss1  8692  ecopovtrn  8834  fpmg  8889  tskord  10858  ltadd2  11407  mul12  11468  add12  11521  addsub  11561  addsubeq4  11565  ppncan  11593  leadd1  11777  ltaddsub2  11784  leaddsub2  11786  ltsub1  11805  ltsub2  11806  div23  11986  ltmul1  12160  ltmulgt11  12169  lediv1  12175  lemuldiv  12190  ltdiv2  12196  zdiv  12762  xltadd1  13379  xltmul1  13415  iooneg  13595  icoshft  13597  fzaddel  13685  fzshftral  13742  modmulmodr  14073  facwordi  14426  pfxeq  14838  abssubge0  15488  climshftlem  15734  dvdsmul1  16440  divalglem8  16563  divalgb  16567  rprpwr  16726  lcmgcdeq  16780  pcfac  17070  mhmmulg  19318  rmodislmodlem  21197  xrsdsreval  21711  cnmptcom  23990  hmeof1o2  24075  ordthmeo  24114  isclmi0  25412  iscvsi  25443  cxplt2  27019  leadds1im  28366  ltadds2  28370  addscan2  28372  axcontlem8  29542  vcdi  31160  isvciOLD  31175  dipdi  31438  dipsubdi  31444  hvadd12  31630  hvmulcom  31638  his5  31681  bcs3  31778  chj12  32129  spansnmul  32159  homul12  32400  hoaddsub  32411  lnopmul  32562  lnopaddmuli  32568  lnopsubmuli  32570  lnfnaddmuli  32640  leop2  32719  dmdsl3  32910  chirredlem3  32987  atmd2  32995  cdj3lem3  33033  signstfvc  35196  3com12d  37079  cnambfre  38566  sdclem2  38656  indstrd  43223  addrcom  45442  uun123p1  45776  sineq0ALT  45904  stoweidlem17  46996  sigaras  47834  sigarms  47835  i0oii  49997