![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ralimdv | GIF version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 8-Oct-2003.) |
Ref | Expression |
---|---|
ralimdv.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
ralimdv | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdv.1 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | 1 | adantr 271 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒)) |
3 | 2 | ralimdva 2442 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1439 ∀wral 2360 |
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 1382 ax-gen 1384 ax-4 1446 ax-17 1465 |
This theorem depends on definitions: df-bi 116 df-nf 1396 df-ral 2365 |
This theorem is referenced by: poss 4134 sess1 4173 sess2 4174 riinint 4707 dffo4 5461 dffo5 5462 isoini2 5612 rdgivallem 6160 iinerm 6378 xpf1o 6614 resqrexlemgt0 10514 cau3lem 10608 caubnd2 10611 climshftlemg 10751 climcau 10797 climcaucn 10801 serf0 10802 modfsummodlemstep 10912 bezoutlemmain 11326 strsetsid 11588 fiinbas 11808 baspartn 11809 rescncf 11910 |
Copyright terms: Public domain | W3C validator |