![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralimdva | GIF version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.) |
Ref | Expression |
---|---|
ralimdva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralimdva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1539 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralimdva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
3 | 1, 2 | ralimdaa 2556 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-4 1521 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-ral 2473 |
This theorem is referenced by: ralimdv 2558 ralimdvva 2559 f1mpt 5793 isores3 5837 caofrss 6132 caoftrn 6133 tfrlemibxssdm 6353 tfr1onlembxssdm 6369 tfrcllembxssdm 6382 tfrcl 6390 infidc 6965 exmidomniim 7170 exmidontri2or 7273 caucvgsrlemoffcau 7828 caucvgsrlemoffres 7830 indstr 9625 caucvgre 11025 rexuz3 11034 resqrexlemgt0 11064 resqrexlemglsq 11066 cau3lem 11158 rexanre 11264 rexico 11265 2clim 11344 climcn1 11351 climcn2 11352 subcn2 11354 climsqz 11378 climsqz2 11379 climcvg1nlem 11392 fprodsplitdc 11639 bezoutlemaz 12039 bezoutlembz 12040 bezoutlembi 12041 pcfac 12385 pockthg 12392 infpnlem1 12394 isgrpinv 13013 dfgrp3me 13059 issubg4m 13149 cncnp 14207 txlm 14256 metequiv2 14473 metcnpi3 14494 rescncf 14545 cncfco 14555 suplociccreex 14579 limcresi 14612 cnplimcim 14613 cnplimclemr 14615 cnlimcim 14617 limccnpcntop 14621 limccoap 14624 2sqlem6 14945 bj-charfunbi 15041 nninffeq 15248 tridceq 15283 |
Copyright terms: Public domain | W3C validator |