MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3com12 Structured version   Visualization version   GIF version

Theorem 3com12 1120
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
StepHypRef Expression
1 3exp.1 . . 3 ((𝜑𝜓𝜒) → 𝜃)
213exp 1116 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp21 1111 1 ((𝜓𝜑𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  3comr  1122  3com23  1123  brelrng  5788  fresaunres1  6532  fvun2  6737  onfununi  7965  oaword  8162  nnaword  8240  nnmword  8246  ecopovtrn  8387  fpmg  8419  tskord  10191  ltadd2  10733  mul12  10794  add12  10846  addsub  10886  addsubeq4  10890  ppncan  10917  leadd1  11097  ltaddsub2  11104  leaddsub2  11106  ltsub1  11125  ltsub2  11126  div23  11306  ltmul1  11479  ltmulgt11  11489  lediv1  11494  lemuldiv  11509  ltdiv2  11515  zdiv  12040  xltadd1  12637  xltmul1  12673  iooneg  12849  icoshft  12851  fzaddel  12936  fzshftral  12990  modmulmodr  13300  facwordi  13645  pfxeq  14049  abssubge0  14678  climshftlem  14922  dvdsmul1  15622  divalglem8  15740  divalgb  15744  lcmgcdeq  15945  pcfac  16224  mhmmulg  18259  rmodislmodlem  19692  xrsdsreval  20134  cnmptcom  22281  hmeof1o2  22366  ordthmeo  22405  isclmi0  23701  iscvsi  23732  cxplt2  25287  axcontlem8  26763  vcdi  28346  isvciOLD  28361  dipdi  28624  dipsubdi  28630  hvadd12  28816  hvmulcom  28824  his5  28867  bcs3  28964  chj12  29315  spansnmul  29345  homul12  29586  hoaddsub  29597  lnopmul  29748  lnopaddmuli  29754  lnopsubmuli  29756  lnfnaddmuli  29826  leop2  29905  dmdsl3  30096  chirredlem3  30173  atmd2  30181  cdj3lem3  30219  signstfvc  31918  3com12d  33732  cnambfre  35064  sdclem2  35139  addrcom  41114  uun123p1  41450  sineq0ALT  41578  stoweidlem17  42599  sigaras  43409  sigarms  43410
  Copyright terms: Public domain W3C validator