![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ad2ant2l | GIF version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
ad2ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad2ant2l | ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantrl 478 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantll 476 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: mpteqb 5602 mpofun 5971 xpdom2 6825 addcmpblnq 7354 addpipqqslem 7356 addpipqqs 7357 addclnq 7362 addcomnqg 7368 addassnqg 7369 mulcomnqg 7370 mulassnqg 7371 distrnqg 7374 ltdcnq 7384 enq0ref 7420 addcmpblnq0 7430 addclnq0 7438 nqpnq0nq 7440 nqnq0a 7441 nqnq0m 7442 distrnq0 7446 mulcomnq0 7447 addassnq0lemcl 7448 genpdisj 7510 appdiv0nq 7551 addcomsrg 7742 mulcomsrg 7744 mulasssrg 7745 distrsrg 7746 addcnsr 7821 mulcnsr 7822 addcnsrec 7829 axaddcl 7851 axmulcl 7853 axaddcom 7857 add42 8106 muladd 8328 mulsub 8345 apreim 8547 divmuleqap 8660 ltmul12a 8803 lemul12b 8804 lemul12a 8805 qaddcl 9621 qmulcl 9623 iooshf 9936 fzass4 10045 elfzomelpfzo 10214 tanaddaplem 11727 opnneissb 13315 neitx 13428 txcnmpt 13433 txrest 13436 metcnp3 13671 cncfmet 13739 dveflem 13847 lgsdir2 14094 |
Copyright terms: Public domain | W3C validator |