![]() |
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 5608 mpofun 5979 xpdom2 6833 addcmpblnq 7368 addpipqqslem 7370 addpipqqs 7371 addclnq 7376 addcomnqg 7382 addassnqg 7383 mulcomnqg 7384 mulassnqg 7385 distrnqg 7388 ltdcnq 7398 enq0ref 7434 addcmpblnq0 7444 addclnq0 7452 nqpnq0nq 7454 nqnq0a 7455 nqnq0m 7456 distrnq0 7460 mulcomnq0 7461 addassnq0lemcl 7462 genpdisj 7524 appdiv0nq 7565 addcomsrg 7756 mulcomsrg 7758 mulasssrg 7759 distrsrg 7760 addcnsr 7835 mulcnsr 7836 addcnsrec 7843 axaddcl 7865 axmulcl 7867 axaddcom 7871 add42 8121 muladd 8343 mulsub 8360 apreim 8562 divmuleqap 8676 ltmul12a 8819 lemul12b 8820 lemul12a 8821 qaddcl 9637 qmulcl 9639 iooshf 9954 fzass4 10064 elfzomelpfzo 10233 tanaddaplem 11748 issubg4m 13058 islmodd 13388 opnneissb 13694 neitx 13807 txcnmpt 13812 txrest 13815 metcnp3 14050 cncfmet 14118 dveflem 14226 lgsdir2 14473 |
Copyright terms: Public domain | W3C validator |