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

Theorem simpl2im 505
Description: Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)
Hypotheses
Ref Expression
simpl2im.1 (𝜑 → (𝜓𝜒))
simpl2im.2 (𝜒𝜃)
Assertion
Ref Expression
simpl2im (𝜑𝜃)

Proof of Theorem simpl2im
StepHypRef Expression
1 simpl2im.1 . . 3 (𝜑 → (𝜓𝜒))
21simprd 497 . 2 (𝜑𝜒)
3 simpl2im.2 . 2 (𝜒𝜃)
42, 3syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  caovmo  7595  curry1  8040  fsuppunfi  9333  oiid  9485  cantnflt  9616  oemapvali  9628  cnfcom2lem  9645  cfeq0  10200  recmulnq  10908  addgt0sr  11048  mappsrpr  11052  isercolllem2  15559  dvdsaddre2b  16197  ndvdssub  16299  lcmfunsn  16528  imasvscafn  17427  subcidcl  17738  funcoppc  17769  clatleglb  18415  sgrpidmnd  18569  conjsubgen  19049  gagrpid  19082  gaass  19085  cntzssv  19116  cntzi  19117  efgredlemf  19531  abveq0  20328  abvmul  20331  abvtri  20332  cnpimaex  22630  restnlly  22856  fclsopni  23389  xmeteq0  23714  xmettri2  23716  metcnpi  23923  metcnpi2  23924  causs  24685  dvbssntr  25287  dgrlem  25613  dgrlb  25620  umgredgne  28145  nbgrcl  28332  wlkdlem3  28681  usgr2trlncrct  28800  wwlksonvtx  28849  wwlksnextproplem3  28905  erclwwlknsym  29063  erclwwlkntr  29064  1pthon2v  29146  cycpmco2lem3  32033  elrspunidl  32258  sseqf  33056  subgrwlk  33790  acycgrsubgr  33816  pr2el2  41915  rfovcnvf1od  42368  gneispaceel  42507  gneispacess  42509  linindslinci  46619  2arymaptfv  46827  f1sn2g  47007
  Copyright terms: Public domain W3C validator