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 281 | 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: ad2antlr 480 ad2ant2l 499 ad2ant2lr 501 3ad2antl3 1130 3adant1l 1193 reu6 2846 sbc2iegf 2951 sbcralt 2957 sbcrext 2958 indifdir 3302 pofun 4204 poinxp 4578 ssimaex 5450 fndmdif 5493 dffo4 5536 fcompt 5558 fconst2g 5603 foco2 5623 foeqcnvco 5659 f1eqcocnv 5660 fliftel1 5663 isores3 5684 acexmid 5741 tfrlemi14d 6198 tfrcl 6229 dom2lem 6634 fiintim 6785 ordiso2 6888 mkvprop 7000 lt2addnq 7180 lt2mulnq 7181 ltexnqq 7184 genpdf 7284 addnqprl 7305 addnqpru 7306 addlocpr 7312 recexprlemopl 7401 caucvgsrlemgt1 7571 add4 7891 cnegex 7908 ltleadd 8176 zextle 9100 peano5uzti 9117 fnn0ind 9125 xrlttr 9536 xaddass 9607 iccshftr 9732 iccshftl 9734 iccdil 9736 icccntr 9738 fzaddel 9794 fzrev 9819 exbtwnzlemshrink 9981 seq3val 10186 iseqf1olemab 10217 exp3vallem 10249 mulexp 10287 expadd 10290 expmul 10293 leexp1a 10303 bccl 10468 hashfacen 10534 ovshftex 10546 2shfti 10558 caucvgre 10708 cvg1nlemcau 10711 resqrexlemcvg 10746 cau3lem 10841 rexico 10948 iooinsup 11001 climmpt 11024 subcn2 11035 climrecvg1n 11072 climcvg1nlem 11073 climcaucn 11075 mertenslem2 11260 eftlcl 11308 reeftlcl 11309 dvdsext 11465 sqoddm1div8z 11495 bezoutlemaz 11603 bezoutr1 11633 dvdslcm 11662 lcmeq0 11664 lcmcl 11665 lcmneg 11667 lcmdvds 11672 coprmgcdb 11681 dvdsprime 11715 cnco 12301 cnss1 12306 tx2cn 12350 upxp 12352 metss 12574 txmetcnp 12598 cncfss 12650 cosz12 12772 bj-findis 13073 |
Copyright terms: Public domain | W3C validator |