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 197  df-an 385
This theorem is referenced by:  rexlimdvv  3066  ralcom2  3133  ssexnelpss  3753  wereu2  5140  oneqmini  5814  suctr  5846  fun11iun  7168  poxp  7334  suppssr  7371  smoel  7502  omabs  7772  omsmo  7779  iiner  7862  fodomr  8152  fisseneq  8212  suplub2  8408  supnub  8409  infglb  8437  infnlb  8439  inf3lem6  8568  cfcoflem  9132  coftr  9133  zorn2lem7  9362  alephreg  9442  inar1  9635  gruen  9672  letr  10169  lbzbi  11814  xrletr  12027  xmullem  12132  supxrun  12184  ssfzoulel  12602  ssfzo12bi  12603  hashbnd  13163  fi1uzind  13317  brfi1indALT  13320  cau3lem  14138  summo  14492  mertenslem2  14661  prodmolem2  14709  alzdvds  15089  nno  15145  nn0seqcvgd  15330  lcmdvds  15368  lcmf  15393  divgcdodd  15469  prmpwdvds  15655  catpropd  16416  pltnle  17013  pltval3  17014  pltletr  17018  tsrlemax  17267  frgpnabllem1  18322  cyggexb  18346  abvn0b  19350  isphld  20047  indistopon  20853  restntr  21034  cnprest  21141  lmss  21150  lmmo  21232  2ndcdisj  21307  txlm  21499  flftg  21847  bndth  22804  iscmet3  23137  bcthlem5  23171  ovolicc2lem4  23334  ellimc3  23688  lhop1  23822  ulmcaulem  24193  ulmcau  24194  ulmcn  24198  xrlimcnp  24740  ax5seglem4  25857  axcontlem2  25890  axcontlem4  25892  incistruhgr  26019  nbuhgr  26284  uhgrnbgr0nb  26295  wwlknp  26791  wwlksnred  26855  clwlkclwwlklem2a  26964  vdgn0frgrv2  27275  nmcvcn  27678  htthlem  27902  atcvat3i  29383  sumdmdlem2  29406  ifeqeqx  29487  bnj23  30912  bnj849  31121  sotr3  31782  funbreq  31794  nosepssdm  31961  cgrdegen  32236  lineext  32308  btwnconn1lem7  32325  btwnconn1lem14  32332  waj-ax  32538  lukshef-ax2  32539  relowlssretop  33341  finxpreclem6  33363  fin2solem  33525  poimirlem2  33541  poimirlem18  33557  poimirlem21  33560  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  unirep  33637  seqpo  33673  ssbnd  33717  intidl  33958  prnc  33996  prtlem15  34479  lshpkrlem6  34720  atlatmstc  34924  cvrat3  35046  ps-2  35082  2lplnj  35224  paddasslem5  35428  dochkrshp4  36995  isnacs3  37590  pm14.24  38950  rexlim2d  40175  iccpartigtl  41684  icceuelpartlem  41696  rngcinv  42306  rngcinvALTV  42318  ringcinv  42357  ringcinvALTV  42381  lindslinindsimp1  42571  lindslinindsimp2  42577  digexp  42726  aacllem  42875
  Copyright terms: Public domain W3C validator