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

Theorem simpl2im 502
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 494 . 2 (𝜑𝜒)
3 simpl2im.2 . 2 (𝜒𝜃)
42, 3syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  caovmo  7658  curry1  8109  fsuppunfi  9413  oiid  9566  cantnflt  9697  oemapvali  9709  cnfcom2lem  9726  cfeq0  10281  recmulnq  10989  addgt0sr  11129  mappsrpr  11133  isercolllem2  15648  dvdsaddre2b  16287  ndvdssub  16389  lcmfunsn  16618  imasvscafn  17522  subcidcl  17833  funcoppc  17864  clatleglb  18513  sgrpidmnd  18702  conjsubgen  19214  gagrpid  19257  gaass  19260  cntzssv  19291  cntzi  19292  efgredlemf  19708  abveq0  20718  abvmul  20721  abvtri  20722  cnpimaex  23204  restnlly  23430  fclsopni  23963  xmeteq0  24288  xmettri2  24290  metcnpi  24497  metcnpi2  24498  causs  25270  dvbssntr  25873  dgrlem  26208  dgrlb  26215  precsexlem11  28165  umgredgne  29030  nbgrcl  29220  wlkdlem3  29570  usgr2trlncrct  29689  wwlksonvtx  29738  wwlksnextproplem3  29794  erclwwlknsym  29952  erclwwlkntr  29953  1pthon2v  30035  cycpmco2lem3  32941  idomsubr  33095  elrspunidl  33240  sseqf  34140  subgrwlk  34870  acycgrsubgr  34896  pr2el2  43120  rfovcnvf1od  43573  gneispaceel  43712  gneispacess  43714  clnbgrcl  47295  linindslinci  47699  2arymaptfv  47907  f1sn2g  48086
  Copyright terms: Public domain W3C validator