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

Theorem expcomd 453
Description: Deduction form of expcom 450. (Contributed by Alan Sare, 22-Jul-2012.)
Hypothesis
Ref Expression
expcomd.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
expcomd (𝜑 → (𝜒 → (𝜓𝜃)))

Proof of Theorem expcomd
StepHypRef Expression
1 expcomd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 451 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  simplbi2comt  655  ralrimdva  2998  reupick  3944  trintssOLD  4803  pwssun  5049  ordelord  5783  tz7.7  5787  ordtr3OLD  5808  poxp  7334  smores2  7496  smoiun  7503  smogt  7509  tz7.49  7585  omsmolem  7778  mapxpen  8167  f1dmvrnfibi  8291  suplub2  8408  epfrs  8645  r1sdom  8675  rankr1ai  8699  ficardom  8825  cardsdomel  8838  dfac5lem5  8988  cfsmolem  9130  cfcoflem  9132  axdc3lem2  9311  zorn2lem7  9362  genpn0  9863  reclem2pr  9908  supsrlem  9970  ltletr  10167  fzind  11513  rpneg  11901  xrltletr  12026  iccid  12258  ssfzoulel  12602  ssfzo12bi  12603  swrdccatin12lem2  13535  swrdccat  13539  repsdf2  13571  repswswrd  13577  cshwcsh2id  13620  o1rlimmul  14393  dvdsabseq  15082  divalgb  15174  bezoutlem3  15305  cncongr1  15428  ncoprmlnprm  15483  difsqpwdvds  15638  lss1d  19011  pf1ind  19767  chfacfisf  20707  chfacfisfcpmat  20708  cayleyhamilton1  20745  txlm  21499  fmfnfmlem1  21805  blsscls2  22356  metcnpi3  22398  bcmono  25047  upgrewlkle2  26558  redwlk  26625  crctcshwlkn0lem5  26762  wwlksnextwrd  26860  clwwlknonex2lem2  27083  ocnel  28285  atcvat2i  29374  atcvat4i  29384  dfon2lem5  31816  sletr  32008  cgrxfr  32287  colinearxfr  32307  hfelhf  32413  isbasisrelowllem1  33333  isbasisrelowllem2  33334  finxpreclem6  33363  seqpo  33673  atlatle  34925  cvrexchlem  35023  cvrat2  35033  cvrat4  35047  pmapjoin  35456  onfrALTlem2  39078  onfrALTlem2VD  39439  eluzge0nn0  41647  elfz2z  41650  iccpartiltu  41683  iccpartigtl  41684  iccpartlt  41685  pfxccatin12lem2  41749  lighneal  41853  bgoldbtbnd  42022  tgoldbach  42030  tgoldbachOLD  42037  cznnring  42281  ply1mulgsumlem2  42500
  Copyright terms: Public domain W3C validator