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

Theorem expdimp 452
Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
Hypothesis
Ref Expression
expd.1 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
expdimp ((𝜑𝜓) → (𝜒𝜃))

Proof of Theorem expdimp
StepHypRef Expression
1 expd.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 451 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 444 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 196  df-an 385
This theorem is referenced by:  rexlimdvv  3019  ralcom2  3083  ssexnelpss  3682  wereu2  5025  oneqmini  5679  suctr  5711  fun11iun  6997  poxp  7154  suppssr  7191  smoel  7322  omabs  7592  omsmo  7599  iiner  7684  fodomr  7974  fisseneq  8034  suplub2  8228  supnub  8229  infglb  8257  infnlb  8259  inf3lem6  8391  cfcoflem  8955  coftr  8956  zorn2lem7  9185  alephreg  9261  inar1  9454  gruen  9491  letr  9983  lbzbi  11611  xrletr  11827  xmullem  11926  supxrun  11977  ssfzoulel  12386  ssfzo12bi  12387  hashbnd  12943  fi1uzind  13083  brfi1indALT  13086  fi1uzindOLD  13089  brfi1indALTOLD  13092  cau3lem  13891  summo  14244  mertenslem2  14405  prodmolem2  14453  alzdvds  14829  nno  14885  nn0seqcvgd  15070  lcmdvds  15108  lcmf  15133  divgcdodd  15209  prmpwdvds  15395  catpropd  16141  pltnle  16738  pltval3  16739  pltletr  16743  tsrlemax  16992  frgpnabllem1  18048  cyggexb  18072  abvn0b  19072  isphld  19766  indistopon  20563  restntr  20744  cnprest  20851  lmss  20860  lmmo  20942  2ndcdisj  21017  txlm  21209  flftg  21558  bndth  22513  iscmet3  22844  bcthlem5  22878  ovolicc2lem4  23040  ellimc3  23394  lhop1  23526  ulmcaulem  23897  ulmcau  23898  ulmcn  23902  xrlimcnp  24440  ax5seglem4  25558  axcontlem2  25591  axcontlem4  25593  clwlkisclwwlklem2a  26107  rusgrasn  26266  frgrawopreglem5  26369  extwwlkfablem2  26399  nmcvcn  26728  htthlem  26952  atcvat3i  28433  sumdmdlem2  28456  ifeqeqx  28539  bnj23  29832  bnj849  30043  funbreq  30708  sltasym  30865  cgrdegen  31075  lineext  31147  btwnconn1lem7  31164  btwnconn1lem14  31171  waj-ax  31377  lukshef-ax2  31378  relowlssretop  32181  finxpreclem6  32203  fin2solem  32359  poimirlem2  32375  poimirlem18  32391  poimirlem21  32394  poimirlem26  32399  poimirlem27  32400  poimirlem31  32404  unirep  32471  seqpo  32507  ssbnd  32551  intidl  32792  prnc  32830  prtlem15  32972  lshpkrlem6  33214  atlatmstc  33418  cvrat3  33540  ps-2  33576  2lplnj  33718  paddasslem5  33922  dochkrshp4  35490  isnacs3  36085  pm14.24  37449  rexlim2d  38486  iccpartigtl  39756  icceuelpartlem  39768  incistruhgr  40297  nbuhgr  40557  uhgrnbgr0nb  40568  wwlknp  41037  wwlksnred  41090  clwlkclwwlklem2a  41199  vdgn0frgrv2  41457  frgrwopreglem5  41477  rngcinv  41765  rngcinvALTV  41777  ringcinv  41816  ringcinvALTV  41840  lindslinindsimp1  42032  lindslinindsimp2  42038  digexp  42191  aacllem  42309
  Copyright terms: Public domain W3C validator