![]() |
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 1476 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralimdva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) | |
3 | 1, 2 | ralimdaa 2457 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 1448 ∀wral 2375 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-4 1455 ax-17 1474 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-ral 2380 |
This theorem is referenced by: ralimdv 2459 ralimdvva 2460 f1mpt 5604 isores3 5648 caofrss 5937 caoftrn 5938 tfrlemibxssdm 6154 tfr1onlembxssdm 6170 tfrcllembxssdm 6183 tfrcl 6191 exmidomniim 6925 caucvgsrlemoffcau 7493 caucvgsrlemoffres 7495 indstr 9238 caucvgre 10593 rexuz3 10602 resqrexlemgt0 10632 resqrexlemglsq 10634 cau3lem 10726 rexanre 10832 rexico 10833 2clim 10909 climcn1 10916 climcn2 10917 subcn2 10919 climsqz 10943 climsqz2 10944 climcvg1nlem 10957 bezoutlemaz 11484 bezoutlembz 11485 bezoutlembi 11486 cncnp 12180 txlm 12229 metequiv2 12424 metcnpi3 12441 rescncf 12481 cncfco 12491 limcresi 12515 cnplimcim 12516 cnlimcim 12517 limccnpcntop 12520 nninffeq 12800 |
Copyright terms: Public domain | W3C validator |