Theorem rcp-NDIMI2 224

Description: → Introduction Recipe. †

Hypothesis

Ref	Expression
rcp-NDIMI2.1	⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)

Assertion

Ref	Expression
rcp-NDIMI2	⊢ (𝛾₁ → (𝛾₂ → 𝜑))

Proof of Theorem rcp-NDIMI2

Step	Hyp	Ref	Expression
1		rcp-NDIMI2.1	. 2 ⊢ ((𝛾₁ ∧ 𝛾₂) → 𝜑)
2	1	ndimi-P3.5 170	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:  axL1-P3.21  252  axL2-P3.22  254  mae-P3.23  257  syl-P3.24  259  rae-P3.26  263  imcomm-P3.27  265  imsubl-P3.28a  267  imsubr-P3.28b  269  trnsp-P3.31a  279  trnsp-P3.31b  282  trnsp-P3.31c  285  trnsp-P3.31d  288  import-P3.34a  305  export-P3.34b  307  example-E3.1a  309  subbil-P3.41a-L1  331  subandl-P3.42a-L1  338  suborl-P3.43a-L1  345  orasim-P3.48-L1  359  impoe-P4.4a  377  nimpoe-P4.4b  380  joinimandinc-P4.8a  397  joinimandres-P4.8b  400  joinimor-P4.8c  403  sepimandr-P4.9a  406  sepimorl-P4.9b  409  trueie-P4.22a  444  imoverim-P4.30-L1  476  dalloverim-P5  590  dalloverimex-P5  605  qimeqex-P5-L2  611  eqmiddle-P6  708  spliteq-P6-L1  775  splitelof-P6-L1  777  splitelof-P6  778  nfradd-P6  781  nfrmult-P6  782  psubsuccv-P6-L1  805  psubaddv-P6-L1  807  psubmultv-P6-L1  809  lemma-L7.02a-L1  943  axL4-P7  945  axL4ex-P7  946  nfrgencl-P7  965  allic-P7  1007  dalloverim-P7  1022  dalloverimex-P7  1033  qimeqex-P7-L1  1054  qimeqex-P7-L2  1055  nfradd-P8  1120  nfrmult-P8  1121