Theorem 3com12 1119

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3comr  1121  3com23  1122  brelrng  5814  fresaunres1  6554  fvun2  6758  onfununi  7981  oaword  8178  nnaword  8256  nnmword  8262  ecopovtrn  8403  fpmg  8435  tskord  10205  ltadd2  10747  mul12  10808  add12  10860  addsub  10900  addsubeq4  10904  ppncan  10931  leadd1  11111  ltaddsub2  11118  leaddsub2  11120  ltsub1  11139  ltsub2  11140  div23  11320  ltmul1  11493  ltmulgt11  11503  lediv1  11508  lemuldiv  11523  ltdiv2  11529  zdiv  12055  xltadd1  12652  xltmul1  12688  iooneg  12860  icoshft  12862  fzaddel  12944  fzshftral  12998  modmulmodr  13308  facwordi  13652  pfxeq  14061  abssubge0  14690  climshftlem  14934  dvdsmul1  15634  divalglem8  15754  divalgb  15758  lcmgcdeq  15959  pcfac  16238  mhmmulg  18271  rmodislmodlem  19704  xrsdsreval  20593  cnmptcom  22289  hmeof1o2  22374  ordthmeo  22413  isclmi0  23705  iscvsi  23736  cxplt2  25284  axcontlem8  26760  vcdi  28345  isvciOLD  28360  dipdi  28623  dipsubdi  28629  hvadd12  28815  hvmulcom  28823  his5  28866  bcs3  28963  chj12  29314  spansnmul  29344  homul12  29585  hoaddsub  29596  lnopmul  29747  lnopaddmuli  29753  lnopsubmuli  29755  lnfnaddmuli  29825  leop2  29904  dmdsl3  30095  chirredlem3  30172  atmd2  30180  cdj3lem3  30218  signstfvc  31848  3com12d  33662  cnambfre  34944  sdclem2  35021  addrcom  40813  uun123p1  41149  sineq0ALT  41277  stoweidlem17  42309  sigaras  43119  sigarms  43120