Theorem rcp-NDIMP0addall 207

Description: ( ) ⇒ ( 1 ∧... ∧ n ). †

Hypothesis

Ref	Expression
rcp-NDIMP0addall.1	⊢ 𝜑

Assertion

Ref	Expression
rcp-NDIMP0addall	⊢ (𝛾 → 𝜑)

Proof of Theorem rcp-NDIMP0addall

Step	Hyp	Ref	Expression
1		rcp-NDIMP0addall.1	. . . . 5 ⊢ 𝜑
2	1	ndtruei-P3.17 182	. . . 4 ⊢ (⊤ → 𝜑)
3	2	ndimp-P3.2 167	. . 3 ⊢ ((⊤ ∧ 𝛾) → 𝜑)
4	3	ndimi-P3.5 170	. 2 ⊢ (⊤ → (𝛾 → 𝜑))
5	4	ndtruee-P3.18 183	1 ⊢ (𝛾 → 𝜑)

Syntax hints:   → wff-imp 10  ⊤wff-true 153

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  df-true-D2.4 155

This theorem is referenced by:  rcp-NDNEGI1  218  rcp-NDORE1  234  ndexclmid-P3.16.AC  251  subbir-P3.41b  334  subandr-P3.42b  341  suborr-P3.43b  348  negbicancel-P4.11  419  negbicancelint-P4.14  424  idandtruel-P4.19a  438  thmeqtrue-P4.21a  442  truthtbltbif-P4.39b  508  truthtblfbit-P4.39c  509  exclmid2peirce-P4.41a  512  andcomm2-P4  564  orcomm2-P4  566  joinimandinc3-P4  578  joinimandres3-P4  582  joinimor2-P4  584  joinimor3-P4  586  alloverim-P5  588  alloverimex-P5  601  qimeqallav-P5-L1  617  qimeqallbv-P5-L1  619  eqsym-P5  627  eqtrns-P5  630  subeql-P5  632  qremallv-P5  656  qremexv-P5  657  example-E5.03a  665  nfrv-P6  686  nfrall1w-P6  692  nfrex1w-P6  693  qimeqalla-P6-L1  698  qimeqallb-P6-L1  700  solvesub-P6a.VR  705  example-E6.01a  706  eqmiddle-P6  708  example-E6.02a  712  exi-P6  718  subnfr-P6  755  spliteq-P6-L1  775  splitelof-P6-L1  777  nfrsucc-P6  780  nfradd-P6  781  nfrmult-P6  782  psubthm-P6  786  psubsuccv-P6-L1  805  psubaddv-P6-L1  807  psubmultv-P6-L1  809  nfrgencl-L6  811  gennfrcl-L6  812  nfrimd-P6  815  qremexd-P6  823  ndexew-P7  867  ndalli-P7.17.RC  883  nfrexgen-P7  931  eqsym-P7  936  lemma-L7.02a-L1  943  lemma-L7.02a  944  axL4-P7  945  axL4ex-P7  946  exia-P7  953  lemma-L7.03  962  gennfrcl-P7  963  qimeqallb-P7  976  qimeqalla-P7  1050  example-E7.1a  1074  example-E7.1b  1075  nfrnegconv-P8  1110  nfrsucc-P8  1119  nfradd-P8  1120  nfrmult-P8  1121