Theorem ndandi-P3.7 172

Description: Natural Deduction: '∧' Introduction Rule.

Deduce the conjunction of two previously deduced WFFs.

Hypotheses

Ref	Expression
ndandi-P3.7.1	⊢ (𝛾 → 𝜑)
ndandi-P3.7.2	⊢ (𝛾 → 𝜓)

Assertion

Ref	Expression
ndandi-P3.7	⊢ (𝛾 → (𝜑 ∧ 𝜓))

Proof of Theorem ndandi-P3.7

Step	Hyp	Ref	Expression
1		ndandi-P3.7.1	. 2 ⊢ (𝛾 → 𝜑)
2		ndandi-P3.7.2	. 2 ⊢ (𝛾 → 𝜓)
3	1, 2	cmb-P2.9c.AC.2SH 139	1 ⊢ (𝛾 → (𝜑 ∧ 𝜓))

Syntax hints:   → wff-imp 10   ∧ wff-and 132

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-and-D2.2 133

This theorem is referenced by:  rcp-NDANDI0  229  export-P3.34b  307  andcomm-P3.35-L1  313  andassoc-P3.36-L1  315  andassoc-P3.36-L2  316  subandl-P3.42a-L1  338  andasim-P3.46-L2  355  dfbi-P3.47  358  nprofeliml-P4.6a  389  nprofelimr-P4.6b  391  joinimandres-P4.8b  400  sepimandr-P4.9a  406  sepimorl-P4.9b  409  idandtruel-P4.19a  438  idempotand-P4.25a  450  dmorgafwd-L4.1  452  dmorgbfwd-L4.3  454  andoveror-P4.27-L1  459  andoveror-P4.27-L2  460  oroverand-P4.27-L3  462  oroverand-P4.27-L4  463  joinimandinc2-P4  576  joinimandinc3-P4  578  joinimandres2-P4  580  joinimandres3-P4  582  eqmiddle-P6  708  lemma-L6.07a-L2  771  spliteq-P6-L1  775  splitelof-P6-L1  777