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  5925  fnunres2  6645  fresaunres1  6748  fvun2  6970  onfununi  8330  oaword  8536  nnaword  8615  nnmword  8621  naddel1  8676  naddss1  8678  ecopovtrn  8820  fpmg  8875  tskord  10789  ltadd2  11338  mul12  11399  add12  11452  addsub  11492  addsubeq4  11496  ppncan  11524  leadd1  11706  ltaddsub2  11713  leaddsub2  11715  ltsub1  11734  ltsub2  11735  div23  11915  ltmul1  12089  ltmulgt11  12098  lediv1  12104  lemuldiv  12119  ltdiv2  12125  zdiv  12691  xltadd1  13308  xltmul1  13344  iooneg  13524  icoshft  13526  fzaddel  13613  fzshftral  13670  modmulmodr  14001  facwordi  14353  pfxeq  14765  abssubge0  15415  climshftlem  15661  dvdsmul1  16367  divalglem8  16490  divalgb  16494  rprpwr  16649  lcmgcdeq  16702  pcfac  16991  mhmmulg  19238  rmodislmodlem  21113  xrsdsreval  21625  cnmptcom  23904  hmeof1o2  23989  ordthmeo  24028  isclmi0  25326  iscvsi  25357  cxplt2  26935  leadds1im  28252  ltadds2  28256  addscan2  28258  axcontlem8  29428  vcdi  31046  isvciOLD  31061  dipdi  31324  dipsubdi  31330  hvadd12  31516  hvmulcom  31524  his5  31567  bcs3  31664  chj12  32015  spansnmul  32045  homul12  32286  hoaddsub  32297  lnopmul  32448  lnopaddmuli  32454  lnopsubmuli  32456  lnfnaddmuli  32526  leop2  32605  dmdsl3  32796  chirredlem3  32873  atmd2  32881  cdj3lem3  32919  signstfvc  35082  3com12d  36930  cnambfre  38417  sdclem2  38492  indstrd  43059  addrcom  45297  uun123p1  45631  sineq0ALT  45759  stoweidlem17  46845  sigaras  47683  sigarms  47684  i0oii  49846