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

Theorem expcomd 420
 Description: Deduction form of expcom 417. (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 419 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32com23 86 1 (𝜑 → (𝜒 → (𝜓𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 This theorem is referenced by:  ancomsd  469  simplbi2comt  505  ralrimdva  3154  reupick  4242  pwssun  5425  ordelord  6188  tz7.7  6192  poxp  7818  smores2  7992  smoiun  7999  smogt  8005  tz7.49  8082  omsmolem  8281  mapxpen  8685  f1dmvrnfibi  8810  suplub2  8927  epfrs  9175  r1sdom  9205  rankr1ai  9229  ficardom  9392  cardsdomel  9405  dfac5lem5  9556  cfsmolem  9699  cfcoflem  9701  axdc3lem2  9880  zorn2lem7  9931  genpn0  10432  reclem2pr  10477  supsrlem  10540  ltletr  10739  fzind  12088  rpneg  12429  xrltletr  12558  iccid  12791  ssfzoulel  13146  ssfzo12bi  13147  pfxccatin12lem2  14104  swrdccat  14108  repsdf2  14151  repswswrd  14157  cshwcsh2id  14201  o1rlimmul  14987  dvdsabseq  15675  divalgb  15765  bezoutlem3  15899  cncongr1  16021  ncoprmlnprm  16078  difsqpwdvds  16233  lss1d  19749  pf1ind  21020  chfacfisf  21500  chfacfisfcpmat  21501  cayleyhamilton1  21538  txlm  22294  fmfnfmlem1  22600  blsscls2  23152  metcnpi3  23194  bcmono  25905  upgrewlkle2  27440  redwlk  27506  crctcshwlkn0lem5  27644  wwlksnextwrd  27727  clwwlknonex2lem2  27937  ocnel  29125  atcvat2i  30214  atcvat4i  30224  onelssex  33127  dfon2lem5  33215  sletr  33448  cgrxfr  33776  colinearxfr  33796  hfelhf  33902  isbasisrelowllem1  34923  isbasisrelowllem2  34924  finxpreclem6  34964  seqpo  35336  atlatle  36767  cvrexchlem  36866  cvrat2  36876  cvrat4  36890  pmapjoin  37299  onfrALTlem2  41423  onfrALTlem2VD  41766  eluzge0nn0  44037  elfz2z  44040  iccpartiltu  44107  iccpartigtl  44108  iccpartlt  44109  lighneal  44297  bgoldbtbnd  44495  tgoldbach  44503  cznnring  44748  ply1mulgsumlem2  44962  itsclc0  45351
 Copyright terms: Public domain W3C validator