![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > adantll | GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
adant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
adantll | ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 109 | . 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑) | |
2 | adant2.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 1, 2 | sylan 279 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: ad2antlr 476 ad2ant2l 495 ad2ant2lr 497 3ad2antl3 1113 3adant1l 1176 reu6 2826 sbc2iegf 2931 sbcralt 2937 sbcrext 2938 indifdir 3279 pofun 4172 poinxp 4546 ssimaex 5414 fndmdif 5457 dffo4 5500 fcompt 5522 fconst2g 5567 foco2 5587 foeqcnvco 5623 f1eqcocnv 5624 fliftel1 5627 isores3 5648 acexmid 5705 tfrlemi14d 6160 tfrcl 6191 dom2lem 6596 fiintim 6746 ordiso2 6835 mkvprop 6943 lt2addnq 7113 lt2mulnq 7114 ltexnqq 7117 genpdf 7217 addnqprl 7238 addnqpru 7239 addlocpr 7245 recexprlemopl 7334 caucvgsrlemgt1 7490 add4 7794 cnegex 7811 ltleadd 8075 zextle 8994 peano5uzti 9011 fnn0ind 9019 xrlttr 9422 xaddass 9493 iccshftr 9618 iccshftl 9620 iccdil 9622 icccntr 9624 fzaddel 9680 fzrev 9705 exbtwnzlemshrink 9867 seq3val 10072 iseqf1olemab 10103 exp3vallem 10135 mulexp 10173 expadd 10176 expmul 10179 leexp1a 10189 bccl 10354 hashfacen 10420 ovshftex 10432 2shfti 10444 caucvgre 10593 cvg1nlemcau 10596 resqrexlemcvg 10631 cau3lem 10726 rexico 10833 iooinsup 10885 climmpt 10908 subcn2 10919 climrecvg1n 10956 climcvg1nlem 10957 climcaucn 10959 mertenslem2 11144 eftlcl 11192 reeftlcl 11193 dvdsext 11348 sqoddm1div8z 11378 bezoutlemaz 11484 bezoutr1 11514 dvdslcm 11543 lcmeq0 11545 lcmcl 11546 lcmneg 11548 lcmdvds 11553 coprmgcdb 11562 dvdsprime 11596 cnco 12171 cnss1 12176 tx2cn 12220 upxp 12222 metss 12422 cncfss 12483 bj-findis 12762 |
Copyright terms: Public domain | W3C validator |