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

Theorem simpl2im 506
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 498 . 2 (𝜑𝜒)
3 simpl2im.2 . 2 (𝜒𝜃)
42, 3syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  caovmo  7363  curry1  7777  fsuppunfi  8831  oiid  8983  cantnflt  9113  oemapvali  9125  cnfcom2lem  9142  cfeq0  9656  recmulnq  10364  addgt0sr  10504  mappsrpr  10508  isercolllem2  15002  dvdsaddre2b  15637  ndvdssub  15738  lcmfunsn  15966  imasvscafn  16789  subcidcl  17093  funcoppc  17124  clatleglb  17715  sgrpidmnd  17895  conjsubgen  18370  gagrpid  18403  gaass  18406  cntzssv  18437  cntzi  18438  efgredlemf  18846  abveq0  19573  abvmul  19576  abvtri  19577  cnpimaex  21840  restnlly  22066  fclsopni  22599  xmeteq0  22924  xmettri2  22926  metcnpi  23130  metcnpi2  23131  causs  23881  dvbssntr  24482  dgrlem  24805  dgrlb  24812  umgredgne  26917  nbgrcl  27104  wlkdlem3  27453  usgr2trlncrct  27571  wwlksonvtx  27620  wwlksnextproplem3  27676  erclwwlknsym  27834  erclwwlkntr  27835  1pthon2v  27917  cycpmco2lem3  30778  sseqf  31658  subgrwlk  32387  acycgrsubgr  32413  pr2el2  40045  rfovcnvf1od  40485  gneispaceel  40628  gneispacess  40630  linindslinci  44648
  Copyright terms: Public domain W3C validator