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  168  imbi1d  331  meredith  1563  nfimt  1823  ax13b  1966  ax12v2  2051  ax12vOLD  2052  ax12vOLDOLD  2053  sbequi  2379  mo3  2511  2mo  2555  sstr2  3595  ssralv  3650  soss  5018  frss  5046  fvn0ssdmfun  6307  tfi  7001  nneneq  8088  wemaplem2  8397  unxpwdom2  8438  cantnfp1lem3  8522  infxpenlem  8781  axpowndlem3  9366  indpi  9674  fzind  11419  injresinj  12526  seqcl2  12756  seqfveq2  12760  seqshft2  12764  monoord  12768  seqsplit  12771  seqid2  12784  seqhomo  12785  seqcoll  13183  rexuzre  14021  rexico  14022  limsupbnd2  14143  rlim2lt  14157  rlim3  14158  lo1le  14311  caurcvg  14336  lcmfunsnlem1  15269  coprmprod  15294  eulerthlem2  15406  ramtlecl  15623  sylow1lem1  17929  efgsrel  18063  elcls3  20792  cncls2  20982  cnntr  20984  filssufilg  21620  ufileu  21628  alexsubALTlem3  21758  tgpt0  21827  isucn2  21988  imasdsf1olem  22083  nmoleub2lem2  22819  ovolicc2lem3  23189  dyadmbllem  23268  dvnres  23595  rlimcnp  24587  xrlimcnp  24590  ftalem2  24695  bcmono  24897  2sqlem6  25043  eupth2lems  26958  mdslmd1lem1  29024  xrge0infss  29361  subfacp1lem6  30867  cvmliftlem7  30973  cvmliftlem10  30976  ss2mcls  31165  mclsax  31166  bj-exlimh  32236  bj-spimt2  32343  mettrifi  33171  diaintclN  35813  dibintclN  35922  dihintcl  36099  mapdh9a  36545  iunrelexp0  37461  imbi12VD  38578  smonoord  40627  ply1mulgsumlem1  41436  setrec1lem2  41702
  Copyright terms: Public domain W3C validator