![]() |
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 110 | . 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜑) | |
2 | adant2.1 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
3 | 1, 2 | sylan 283 | 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: ad2antlr 489 ad2ant2l 508 ad2ant2lr 510 ad5ant23 522 ad5ant24 523 ad5ant25 524 3ad2antl3 1161 3adant1l 1230 reu6 2926 sbc2iegf 3033 sbcralt 3039 sbcrext 3040 indifdir 3391 pofun 4308 poinxp 4691 ssimaex 5572 fndmdif 5616 dffo4 5659 fcompt 5681 fconst2g 5726 foco2 5748 foeqcnvco 5784 f1eqcocnv 5785 fliftel1 5788 isores3 5809 acexmid 5867 tfrlemi14d 6327 tfrcl 6358 dom2lem 6765 fiintim 6921 ordiso2 7027 mkvprop 7149 lt2addnq 7381 lt2mulnq 7382 ltexnqq 7385 genpdf 7485 addnqprl 7506 addnqpru 7507 addlocpr 7513 recexprlemopl 7602 caucvgsrlemgt1 7772 add4 8095 cnegex 8112 ltleadd 8380 zextle 9320 peano5uzti 9337 fnn0ind 9345 xrlttr 9769 xaddass 9843 iccshftr 9968 iccshftl 9970 iccdil 9972 icccntr 9974 fzaddel 10032 fzrev 10057 exbtwnzlemshrink 10222 seq3val 10431 iseqf1olemab 10462 exp3vallem 10494 mulexp 10532 expadd 10535 expmul 10538 leexp1a 10548 bccl 10718 hashfacen 10787 ovshftex 10799 2shfti 10811 caucvgre 10961 cvg1nlemcau 10964 resqrexlemcvg 10999 cau3lem 11094 rexico 11201 iooinsup 11256 climmpt 11279 subcn2 11290 climrecvg1n 11327 climcvg1nlem 11328 climcaucn 11330 mertenslem2 11515 eftlcl 11667 reeftlcl 11668 dvdsext 11831 sqoddm1div8z 11861 bezoutlemaz 11974 bezoutr1 12004 dvdslcm 12039 lcmeq0 12041 lcmcl 12042 lcmneg 12044 lcmdvds 12049 coprmgcdb 12058 dvdsprime 12092 pc2dvds 12299 prmpwdvds 12323 infpnlem1 12327 1arith 12335 mhmco 12751 mhmima 12752 dfgrp2 12779 mulgfng 12863 cnco 13354 cnss1 13359 tx2cn 13403 upxp 13405 metss 13627 txmetcnp 13651 cncfss 13703 cosz12 13834 bj-findis 14353 |
Copyright terms: Public domain | W3C validator |