![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad2antll | GIF version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) |
Ref | Expression |
---|---|
ad2ant.1 | ⊢ (φ → ψ) |
Ref | Expression |
---|---|
ad2antll | ⊢ ((χ ∧ (θ ∧ φ)) → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 ⊢ (φ → ψ) | |
2 | 1 | adantl 262 | . 2 ⊢ ((θ ∧ φ) → ψ) |
3 | 2 | adantl 262 | 1 ⊢ ((χ ∧ (θ ∧ φ)) → ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem is referenced by: simprr 484 simprrl 491 simprrr 492 dn1dc 866 prneimg 3536 f1oprg 5111 subhalfnqq 6397 nqnq0pi 6421 genprndl 6504 genprndu 6505 addlocpr 6519 nqprl 6533 addnqprlemrl 6538 addnqprlemru 6539 mullocpr 6552 ltaprlem 6591 aptiprleml 6611 cauappcvgprlemladdfu 6626 cauappcvgprlemladdfl 6627 caucvgprlemladdfu 6648 mulcmpblnrlemg 6668 recexgt0sr 6701 pitonn 6744 rimul 7369 receuap 7432 peano5uzti 8122 iooshf 8591 iseqfveq2 8905 expcl2lemap 8921 mulexpzap 8949 expnlbnd2 9027 |
Copyright terms: Public domain | W3C validator |