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

Theorem expcomd 417
Description: Deduction form of expcom 414. (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 416 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 1 (𝜑 → (𝜒 → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  ancomsd  466  simplbi2comt  502  ralrimdva  3186  reupick  4284  pwssun  5448  ordelord  6206  tz7.7  6210  poxp  7811  smores2  7980  smoiun  7987  smogt  7993  tz7.49  8070  omsmolem  8269  mapxpen  8671  f1dmvrnfibi  8796  suplub2  8913  epfrs  9161  r1sdom  9191  rankr1ai  9215  ficardom  9378  cardsdomel  9391  dfac5lem5  9541  cfsmolem  9680  cfcoflem  9682  axdc3lem2  9861  zorn2lem7  9912  genpn0  10413  reclem2pr  10458  supsrlem  10521  ltletr  10720  fzind  12068  rpneg  12409  xrltletr  12538  iccid  12771  ssfzoulel  13119  ssfzo12bi  13120  pfxccatin12lem2  14081  swrdccat  14085  repsdf2  14128  repswswrd  14134  cshwcsh2id  14178  o1rlimmul  14963  dvdsabseq  15651  divalgb  15743  bezoutlem3  15877  cncongr1  15999  ncoprmlnprm  16056  difsqpwdvds  16211  lss1d  19664  pf1ind  20446  chfacfisf  21390  chfacfisfcpmat  21391  cayleyhamilton1  21428  txlm  22184  fmfnfmlem1  22490  blsscls2  23041  metcnpi3  23083  bcmono  25780  upgrewlkle2  27315  redwlk  27381  crctcshwlkn0lem5  27519  wwlksnextwrd  27602  clwwlknonex2lem2  27814  ocnel  29002  atcvat2i  30091  atcvat4i  30101  dfon2lem5  32929  sletr  33134  cgrxfr  33413  colinearxfr  33433  hfelhf  33539  isbasisrelowllem1  34518  isbasisrelowllem2  34519  finxpreclem6  34559  seqpo  34903  atlatle  36336  cvrexchlem  36435  cvrat2  36445  cvrat4  36459  pmapjoin  36868  onfrALTlem2  40757  onfrALTlem2VD  41100  eluzge0nn0  43389  elfz2z  43392  iccpartiltu  43459  iccpartigtl  43460  iccpartlt  43461  lighneal  43653  bgoldbtbnd  43851  tgoldbach  43859  cznnring  44155  ply1mulgsumlem2  44369  itsclc0  44686
  Copyright terms: Public domain W3C validator