Theorem ndorir-P3.11 176

Description: Natural Deduction: Right '∨' Introduction Rule.

Deduce a new disjunction containing an arbitrary WFF to the right of a previously deduced WFF.

Hypothesis

Ref	Expression
ndorir-P3.11.1	⊢ (𝛾 → 𝜑)

Assertion

Ref	Expression
ndorir-P3.11	⊢ (𝛾 → (𝜑 ∨ 𝜓))

Proof of Theorem ndorir-P3.11

Step	Hyp	Ref	Expression
1		ndorir-P3.11.1	. 2 ⊢ (𝛾 → 𝜑)
2	1	orintr-P2.11b.AC.SH 149	1 ⊢ (𝛾 → (𝜑 ∨ 𝜓))

Syntax hints:   → wff-imp 10   ∨ wff-or 144

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem depends on definitions:  df-bi-D2.1 107  df-or-D2.3 145

This theorem is referenced by:  rcp-NDORIR0  233  ndorir-P3.11.CL  246  orcomm-P3.37-L1  318  orassoc-P3.38-L1  320  orassoc-P3.38-L2  321  suborl-P3.43a-L1  345  orasim-P3.48-L2  360  norer-P4.2b  370  joinimandinc-P4.8a  397  joinimor-P4.8c  403  sepimorl-P4.9b  409  sepimorr-P4.9c  412  sepimandl-P4.9d  415  andoveror-P4.27-L1  459  andoveror-P4.27-L2  460  oroverand-P4.27-L3  462  oroverand-P4.27-L4  463  oroverim-P4.28-L2  466  imasor-P4.32-L1  485