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

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

Proof of Theorem expdimp
StepHypRef Expression
1 expdimp.1 . . 3 (𝜑 → ((𝜓𝜒) → 𝜃))
21expd 404 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 395 1 ((𝜑𝜓) → (𝜒𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  rexlimdvv  3184  ralcom2  3251  ssexnelpss  3881  wereu2  5274  oneqmini  5959  suctr  5991  fun11iun  7324  poxp  7491  suppssr  7529  smoel  7661  omabs  7932  omsmo  7939  iiner  8022  fodomr  8318  fisseneq  8378  suplub2  8574  supnub  8575  infglb  8603  infnlb  8605  inf3lem6  8745  cfcoflem  9347  coftr  9348  zorn2lem7  9577  alephreg  9657  inar1  9850  gruen  9887  letr  10385  lbzbi  11977  xrletr  12191  xmullem  12296  supxrun  12348  ssfzoulel  12770  ssfzo12bi  12771  hashbnd  13327  fi1uzind  13480  brfi1indALT  13483  cau3lem  14381  summo  14735  mertenslem2  14902  prodmolem2  14950  alzdvds  15329  nno  15382  nn0seqcvgd  15566  lcmdvds  15604  lcmf  15629  divgcdodd  15703  prmpwdvds  15889  catpropd  16636  pltnle  17234  pltval3  17235  pltletr  17239  tsrlemax  17488  frgpnabllem1  18542  cyggexb  18566  abvn0b  19576  isphld  20274  indistopon  21085  restntr  21266  cnprest  21373  lmss  21382  lmmo  21464  2ndcdisj  21539  txlm  21731  flftg  22079  bndth  23036  iscmet3  23370  bcthlem5  23405  ovolicc2lem4  23578  ellimc3  23934  lhop1  24068  ulmcaulem  24439  ulmcau  24440  ulmcn  24444  xrlimcnp  24986  ax5seglem4  26103  axcontlem2  26136  axcontlem4  26138  incistruhgr  26251  nbuhgr  26518  uhgrnbgr0nb  26529  wwlknp  27027  wwlksnred  27092  clwlkclwwlklem2a  27204  vdgn0frgrv2  27533  nmcvcn  27941  htthlem  28165  atcvat3i  29646  sumdmdlem2  29669  ifeqeqx  29745  bnj23  31167  bnj849  31375  sotr3  32033  funbreq  32045  nosepssdm  32212  cgrdegen  32487  lineext  32559  btwnconn1lem7  32576  btwnconn1lem14  32583  waj-ax  32784  lukshef-ax2  32785  relowlssretop  33576  finxpreclem6  33598  fin2solem  33751  poimirlem2  33767  poimirlem18  33783  poimirlem21  33786  poimirlem26  33791  poimirlem27  33792  poimirlem31  33796  unirep  33862  seqpo  33897  ssbnd  33941  intidl  34182  prnc  34220  prtlem15  34763  lshpkrlem6  35003  atlatmstc  35207  cvrat3  35330  ps-2  35366  2lplnj  35508  paddasslem5  35712  dochkrshp4  37277  isnacs3  37883  pm14.24  39238  rexlim2d  40427  iccpartigtl  42025  icceuelpartlem  42037  rngcinv  42582  rngcinvALTV  42594  ringcinv  42633  ringcinvALTV  42657  lindslinindsimp1  42847  lindslinindsimp2  42853  digexp  43002  aacllem  43151
  Copyright terms: Public domain W3C validator