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

Theorem imim1d 82
Description: Deduction adding nested consequents. Deduction associated with imim1 83 and imim1i 63. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.)
Hypothesis
Ref Expression
imim1d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
imim1d (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))

Proof of Theorem imim1d
StepHypRef Expression
1 imim1d.1 . 2 (𝜑 → (𝜓𝜒))
2 idd 24 . 2 (𝜑 → (𝜃𝜃))
31, 2imim12d 81 1 (𝜑 → ((𝜒𝜃) → (𝜓𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1  83  expt  178  imbi1d  343  meredith  1633  ax13b  2030  ax12v2  2169  sbequivvOLD  2326  axc15  2438  sbequiOLD  2530  sbequiALT  2592  mo3  2644  mo4  2646  2mo  2729  sstr2  3973  ssralv  4032  axprlem1  5315  axprlem2  5316  axpr  5320  frss  5516  fvn0ssdmfun  6835  tfi  7556  nneneq  8689  wemaplem2  9000  unxpwdom2  9041  cantnfp1lem3  9132  infxpenlem  9428  axpowndlem3  10010  indpi  10318  fzind  12069  injresinj  13148  seqcl2  13378  seqfveq2  13382  seqshft2  13386  monoord  13390  seqsplit  13393  seqid2  13406  seqhomo  13407  seqcoll  13812  rexuzre  14702  rexico  14703  limsupbnd2  14830  rlim2lt  14844  rlim3  14845  lo1le  14998  caurcvg  15023  lcmfunsnlem1  15971  coprmprod  15995  eulerthlem2  16109  ramtlecl  16326  sylow1lem1  18654  efgsrel  18791  elcls3  21621  cncls2  21811  cnntr  21813  filssufilg  22449  ufileu  22457  alexsubALTlem3  22587  tgpt0  22656  isucn2  22817  imasdsf1olem  22912  nmoleub2lem2  23649  ovolicc2lem3  24049  dyadmbllem  24129  dvnres  24457  rlimcnp  25471  xrlimcnp  25474  ftalem2  25579  bcmono  25781  2sqlem6  25927  eupth2lems  27945  mdslmd1lem1  30030  xrge0infss  30411  subfacp1lem6  32330  cvmliftlem7  32436  cvmliftlem10  32439  ss2mcls  32713  mclsax  32714  bj-sylget  33852  bj-nfimt  33869  bj-19.21t  33996  bj-19.37im  33999  bj-spimt2  34005  mettrifi  34915  diaintclN  38076  dibintclN  38185  dihintcl  38362  mapdh9a  38807  iunrelexp0  39927  mnuop3d  40487  imbi12VD  41087  monoordxrv  41638  smonoord  43412  ply1mulgsumlem1  44338  setrec1lem2  44689
  Copyright terms: Public domain W3C validator