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 867 prneimg 3545 f1oprg 5168 fidceq 6330 fidifsnen 6331 php5fin 6339 findcard2d 6348 findcard2sd 6349 diffisn 6350 subhalfnqq 6512 nqnq0pi 6536 genprndl 6619 genprndu 6620 addlocpr 6634 nqprl 6649 nqpru 6650 addnqprlemrl 6655 addnqprlemru 6656 mullocpr 6669 mulnqprlemrl 6671 mulnqprlemru 6672 ltaprlem 6716 aptiprleml 6737 cauappcvgprlemladdfu 6752 cauappcvgprlemladdfl 6753 caucvgprlemladdfu 6775 caucvgprprlemloc 6801 mulcmpblnrlemg 6825 recexgt0sr 6858 pitonn 6924 rereceu 6963 rimul 7576 receuap 7650 peano5uzti 8346 iooshf 8821 iseqfveq2 9228 expcl2lemap 9267 mulexpzap 9295 expnlbnd2 9374 absexpzap 9676 |
Copyright terms: Public domain | W3C validator |