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  177  imbi1d  342  meredith  1644  ax13b  2036  ax12v2  2174  axc15  2421  mo3  2559  mo4  2561  2mo  2645  sstr2  3952  ssralv  4011  axprlem1  5379  axprlem2  5380  axpr  5384  frss  5601  fvn0ssdmfun  7026  tfi  7790  nneneq  9156  nneneqOLD  9168  wemaplem2  9488  unxpwdom2  9529  cantnfp1lem3  9621  infxpenlem  9954  axpowndlem3  10540  indpi  10848  fzind  12606  injresinj  13699  seqcl2  13932  seqfveq2  13936  seqshft2  13940  monoord  13944  seqsplit  13947  seqid2  13960  seqhomo  13961  seqcoll  14369  rexuzre  15243  rexico  15244  limsupbnd2  15371  rlim2lt  15385  rlim3  15386  lo1le  15542  caurcvg  15567  lcmfunsnlem1  16518  coprmprod  16542  eulerthlem2  16659  ramtlecl  16877  sylow1lem1  19385  efgsrel  19521  elcls3  22450  cncls2  22640  cnntr  22642  filssufilg  23278  ufileu  23286  alexsubALTlem3  23416  tgpt0  23486  isucn2  23647  imasdsf1olem  23742  nmoleub2lem2  24495  ovolicc2lem3  24899  dyadmbllem  24979  dvnres  25311  rlimcnp  26331  xrlimcnp  26334  ftalem2  26439  bcmono  26641  2sqlem6  26787  eupth2lems  29224  mdslmd1lem1  31309  xrge0infss  31712  subfacp1lem6  33836  cvmliftlem7  33942  cvmliftlem10  33945  ss2mcls  34219  mclsax  34220  bj-sylget  35131  bj-nfimt  35148  bj-19.21t  35280  bj-19.37im  35283  bj-spimt2  35296  mettrifi  36262  diaintclN  39567  dibintclN  39676  dihintcl  39853  mapdh9a  40298  fltaccoprm  41021  fltabcoprm  41023  flt4lem5  41031  cantnfresb  41702  safesnsupfiub  41776  iunrelexp0  42062  mnuop3d  42639  imbi12VD  43243  monoordxrv  43803  natlocalincr  45201  fcoresf1  45389  rexrsb  45418  smonoord  45649  ply1mulgsumlem1  46553  setrec1lem2  47219  pgindnf  47247
  Copyright terms: Public domain W3C validator