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

Theorem orim2i 897
Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
Hypothesis
Ref Expression
orim1i.1 (𝜑𝜓)
Assertion
Ref Expression
orim2i ((𝜒𝜑) → (𝜒𝜓))

Proof of Theorem orim2i
StepHypRef Expression
1 id 22 . 2 (𝜒𝜒)
2 orim1i.1 . 2 (𝜑𝜓)
31, 2orim12i 895 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 836
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 199  df-or 837
This theorem is referenced by:  orbi2i  899  pm1.5  906  pm2.3  911  r19.44v  3280  elpwunsn  4452  elsuci  6042  infxpenlem  9169  fin1a2lem12  9568  fin1a2  9572  entri3  9716  zindd  11830  elfzr  12900  hashnn0pnf  13447  limccnp  24092  tgldimor  25853  ex-natded5.7-2  27844  chirredi  29825  meran1  32993  dissym1  33003  ordtoplem  33017  ordcmp  33029  poimirlem31  34066
  Copyright terms: Public domain W3C validator