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

Theorem expcomd 418
Description: Deduction form of expcom 415. (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 417 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ancomsd  467  simplbi2comt  503  ralrimdva  3152  reupick  4283  pwssun  5533  ordelord  6344  tz7.7  6348  onelssex  6370  poxp  8065  smores2  8305  smoiun  8312  smogt  8318  tz7.49  8396  omsmolem  8608  mapxpen  9094  f1dmvrnfibi  9287  suplub2  9404  epfrs  9674  r1sdom  9717  rankr1ai  9741  ficardom  9904  cardsdomel  9917  dfac5lem5  10070  cfsmolem  10213  cfcoflem  10215  axdc3lem2  10394  zorn2lem7  10445  genpn0  10946  reclem2pr  10991  supsrlem  11054  ltletr  11254  fzind  12608  rpneg  12954  xrltletr  13083  iccid  13316  ssfzoulel  13673  ssfzo12bi  13674  pfxccatin12lem2  14626  swrdccat  14630  repsdf2  14673  repswswrd  14679  cshwcsh2id  14724  o1rlimmul  15508  dvdsabseq  16202  divalgb  16293  bezoutlem3  16429  cncongr1  16550  ncoprmlnprm  16610  difsqpwdvds  16766  lss1d  20440  pf1ind  21737  chfacfisf  22219  chfacfisfcpmat  22220  cayleyhamilton1  22257  txlm  23015  fmfnfmlem1  23321  blsscls2  23876  metcnpi3  23918  bcmono  26641  sletr  27122  upgrewlkle2  28596  redwlk  28662  crctcshwlkn0lem5  28801  wwlksnextwrd  28884  clwwlknonex2lem2  29094  ocnel  30282  atcvat2i  31371  atcvat4i  31381  dfon2lem5  34401  cgrxfr  34669  colinearxfr  34689  hfelhf  34795  isbasisrelowllem1  35855  isbasisrelowllem2  35856  finxpreclem6  35896  seqpo  36235  atlatle  37811  cvrexchlem  37911  cvrat2  37921  cvrat4  37935  pmapjoin  38344  onfrALTlem2  42902  onfrALTlem2VD  43245  eluzge0nn0  45618  elfz2z  45621  iccpartiltu  45688  iccpartigtl  45689  iccpartlt  45690  lighneal  45877  bgoldbtbnd  46075  tgoldbach  46083  cznnring  46328  ply1mulgsumlem2  46542  itsclc0  46931
  Copyright terms: Public domain W3C validator