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  180  imbi1d  345  meredith  1643  ax13b  2039  ax12v2  2180  sbequivvOLD  2335  axc15  2445  sbequiOLD  2534  sbequiALT  2596  mo3  2647  mo4  2649  2mo  2734  sstr2  3949  ssralv  4008  axprlem1  5301  axprlem2  5302  axpr  5306  frss  5499  fvn0ssdmfun  6824  tfi  7553  nneneq  8688  wemaplem2  8999  unxpwdom2  9040  cantnfp1lem3  9131  infxpenlem  9428  axpowndlem3  10010  indpi  10318  fzind  12068  injresinj  13153  seqcl2  13384  seqfveq2  13388  seqshft2  13392  monoord  13396  seqsplit  13399  seqid2  13412  seqhomo  13413  seqcoll  13818  rexuzre  14703  rexico  14704  limsupbnd2  14831  rlim2lt  14845  rlim3  14846  lo1le  14999  caurcvg  15024  lcmfunsnlem1  15970  coprmprod  15994  eulerthlem2  16108  ramtlecl  16325  sylow1lem1  18714  efgsrel  18851  elcls3  21686  cncls2  21876  cnntr  21878  filssufilg  22514  ufileu  22522  alexsubALTlem3  22652  tgpt0  22722  isucn2  22883  imasdsf1olem  22978  nmoleub2lem2  23719  ovolicc2lem3  24121  dyadmbllem  24201  dvnres  24532  rlimcnp  25549  xrlimcnp  25552  ftalem2  25657  bcmono  25859  2sqlem6  26005  eupth2lems  28021  mdslmd1lem1  30106  xrge0infss  30494  subfacp1lem6  32506  cvmliftlem7  32612  cvmliftlem10  32615  ss2mcls  32889  mclsax  32890  bj-sylget  34028  bj-nfimt  34045  bj-19.21t  34174  bj-19.37im  34177  bj-spimt2  34183  mettrifi  35153  diaintclN  38312  dibintclN  38421  dihintcl  38598  mapdh9a  39043  iunrelexp0  40333  mnuop3d  40913  imbi12VD  41513  monoordxrv  42060  rexrsb  43594  smonoord  43827  ply1mulgsumlem1  44733  setrec1lem2  45157
  Copyright terms: Public domain W3C validator