Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexlimdvva | GIF version |
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.) |
Ref | Expression |
---|---|
rexlimdvva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
rexlimdvva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimdvva.1 | . . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 → 𝜒)) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))) |
3 | 2 | rexlimdvv 2588 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2135 ∃wrex 2443 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-i5r 1522 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-ral 2447 df-rex 2448 |
This theorem is referenced by: ovelrn 5981 f1o2ndf1 6187 eroveu 6583 eroprf 6585 genipv 7441 genpelvl 7444 genpelvu 7445 genprndl 7453 genprndu 7454 addlocpr 7468 addnqprlemrl 7489 addnqprlemru 7490 mulnqprlemrl 7505 mulnqprlemru 7506 ltsopr 7528 ltaddpr 7529 ltexprlemfl 7541 ltexprlemrl 7542 ltexprlemfu 7543 ltexprlemru 7544 cauappcvgprlemladdfu 7586 cauappcvgprlemladdfl 7587 caucvgprlemdisj 7606 caucvgprlemladdfu 7609 caucvgprprlemdisj 7634 apreap 8476 apreim 8492 apirr 8494 apsym 8495 apcotr 8496 apadd1 8497 apneg 8500 mulext1 8501 apti 8511 aprcl 8535 qapne 9568 qtri3or 10168 exbtwnzlemex 10175 rebtwn2z 10180 cjap 10834 rexanre 11148 climcn2 11236 summodc 11310 prodmodclem2 11504 prodmodc 11505 eirrap 11704 dvds2lem 11729 bezoutlemnewy 11914 bezoutlembi 11923 dvdsmulgcd 11943 divgcdcoprm0 12012 cncongr1 12014 sqrt2irrap 12091 pcqmul 12214 pcneg 12235 pcadd 12250 restbasg 12715 txbas 12805 blin2 12979 xmettxlem 13056 xmettx 13057 addcncntoplem 13098 mulcncf 13138 logbgcd1irr 13432 logbgcd1irrap 13435 |
Copyright terms: Public domain | W3C validator |