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

Theorem expdimp 453
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 416 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
32imp 407 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:  rexlimdvv  3297  ralcom2w  3367  ralcom2  3368  ssexnelpss  4093  wereu2  5550  oneqmini  6239  suctr  6271  fiunlemw  7634  fiunlem  7637  poxp  7816  suppssr  7855  smoel  7991  omabs  8267  omsmo  8274  iiner  8362  fodomr  8660  fisseneq  8721  suplub2  8917  supnub  8918  infglb  8946  infnlb  8948  inf3lem6  9088  cfcoflem  9686  coftr  9687  zorn2lem7  9916  alephreg  9996  inar1  10189  gruen  10226  letr  10726  lbzbi  12328  xrletr  12544  xmullem  12650  supxrun  12702  ssfzoulel  13124  ssfzo12bi  13125  hashbnd  13689  fi1uzind  13848  brfi1indALT  13851  cau3lem  14707  summo  15066  mertenslem2  15233  prodmolem2  15281  alzdvds  15662  nno  15725  nn0seqcvgd  15906  lcmdvds  15944  lcmf  15969  2mulprm  16029  divgcdodd  16046  prmpwdvds  16232  catpropd  16971  pltnle  17568  pltval3  17569  pltletr  17573  tsrlemax  17822  frgpnabllem1  18915  cyggexb  18941  abvn0b  19996  isphld  20714  indistopon  21525  restntr  21706  cnprest  21813  lmss  21822  lmmo  21904  2ndcdisj  21980  txlm  22172  flftg  22520  bndth  23477  iscmet3  23811  bcthlem5  23846  ovolicc2lem4  24036  ellimc3  24392  lhop1  24526  ulmcaulem  24897  ulmcau  24898  ulmcn  24902  xrlimcnp  25460  ax5seglem4  26632  axcontlem2  26665  axcontlem4  26667  incistruhgr  26778  nbuhgr  27039  uhgrnbgr0nb  27050  wwlknp  27535  wwlksnred  27584  clwlkclwwlklem2a  27690  vdgn0frgrv2  27988  nmcvcn  28386  htthlem  28608  atcvat3i  30087  sumdmdlem2  30110  ifeqeqx  30211  bnj23  31874  bnj849  32083  prsrcmpltd  32231  cusgr3cyclex  32267  satffunlem2lem1  32535  sotr3  32886  funbreq  32897  nosepssdm  33074  cgrdegen  33349  lineext  33421  btwnconn1lem7  33438  btwnconn1lem14  33445  waj-ax  33646  lukshef-ax2  33647  relowlssretop  34513  finxpreclem6  34546  pibt2  34567  fin2solem  34745  poimirlem2  34761  poimirlem18  34777  poimirlem21  34780  poimirlem26  34785  poimirlem27  34786  poimirlem31  34790  unirep  34856  seqpo  34890  ssbnd  34934  intidl  35175  prnc  35213  prtlem15  35878  lshpkrlem6  36118  atlatmstc  36322  cvrat3  36445  ps-2  36481  2lplnj  36623  paddasslem5  36827  dochkrshp4  38392  rexlimdv3d  39141  isnacs3  39168  pm14.24  40625  rexlim2d  41767  iccpartigtl  43411  icceuelpartlem  43423  prproropf1olem4  43496  rngcinv  44080  rngcinvALTV  44092  ringcinv  44131  ringcinvALTV  44155  lindslinindsimp1  44340  lindslinindsimp2  44346  digexp  44495  aacllem  44730
  Copyright terms: Public domain W3C validator