![]() |
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 470 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantll 468 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: mpteqb 5519 mpofun 5881 xpdom2 6733 addcmpblnq 7199 addpipqqslem 7201 addpipqqs 7202 addclnq 7207 addcomnqg 7213 addassnqg 7214 mulcomnqg 7215 mulassnqg 7216 distrnqg 7219 ltdcnq 7229 enq0ref 7265 addcmpblnq0 7275 addclnq0 7283 nqpnq0nq 7285 nqnq0a 7286 nqnq0m 7287 distrnq0 7291 mulcomnq0 7292 addassnq0lemcl 7293 genpdisj 7355 appdiv0nq 7396 addcomsrg 7587 mulcomsrg 7589 mulasssrg 7590 distrsrg 7591 addcnsr 7666 mulcnsr 7667 addcnsrec 7674 axaddcl 7696 axmulcl 7698 axaddcom 7702 add42 7948 muladd 8170 mulsub 8187 apreim 8389 divmuleqap 8501 ltmul12a 8642 lemul12b 8643 lemul12a 8644 qaddcl 9454 qmulcl 9456 iooshf 9765 fzass4 9873 elfzomelpfzo 10039 tanaddaplem 11481 opnneissb 12363 neitx 12476 txcnmpt 12481 txrest 12484 metcnp3 12719 cncfmet 12787 dveflem 12895 |
Copyright terms: Public domain | W3C validator |