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  5876  fnunres2  6589  fresaunres1  6691  fvun2  6909  onfununi  8256  oaword  8459  nnaword  8537  nnmword  8543  naddel1  8597  naddss1  8599  ecopovtrn  8739  fpmg  8787  tskord  10666  ltadd2  11212  mul12  11273  add12  11326  addsub  11366  addsubeq4  11370  ppncan  11398  leadd1  11580  ltaddsub2  11587  leaddsub2  11589  ltsub1  11608  ltsub2  11609  div23  11790  ltmul1  11966  ltmulgt11  11976  lediv1  11982  lemuldiv  11997  ltdiv2  12003  zdiv  12538  xltadd1  13150  xltmul1  13186  iooneg  13366  icoshft  13368  fzaddel  13453  fzshftral  13510  modmulmodr  13839  facwordi  14191  pfxeq  14598  abssubge0  15230  climshftlem  15476  dvdsmul1  16183  divalglem8  16306  divalgb  16310  rprpwr  16465  lcmgcdeq  16518  pcfac  16806  mhmmulg  19023  rmodislmodlem  20857  xrsdsreval  21343  cnmptcom  23588  hmeof1o2  23673  ordthmeo  23712  isclmi0  25020  iscvsi  25051  cxplt2  26629  sleadd1im  27925  sltadd2  27929  addscan2  27931  axcontlem8  28944  vcdi  30537  isvciOLD  30552  dipdi  30815  dipsubdi  30821  hvadd12  31007  hvmulcom  31015  his5  31058  bcs3  31155  chj12  31506  spansnmul  31536  homul12  31777  hoaddsub  31788  lnopmul  31939  lnopaddmuli  31945  lnopsubmuli  31947  lnfnaddmuli  32017  leop2  32096  dmdsl3  32287  chirredlem3  32364  atmd2  32372  cdj3lem3  32410  signstfvc  34579  3com12d  36344  cnambfre  37708  sdclem2  37782  indstrd  42226  addrcom  44507  uun123p1  44841  sineq0ALT  44969  stoweidlem17  46055  sigaras  46893  sigarms  46894  i0oii  48951