![]() |
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 1163 3adant1l 1232 reu6 2941 sbc2iegf 3048 sbcralt 3054 sbcrext 3055 indifdir 3406 pofun 4330 poinxp 4713 ssimaex 5598 fndmdif 5642 dffo4 5685 fcompt 5707 fconst2g 5752 foco2 5775 foeqcnvco 5812 f1eqcocnv 5813 fliftel1 5816 isores3 5837 acexmid 5896 tfrlemi14d 6359 tfrcl 6390 dom2lem 6799 fiintim 6958 ordiso2 7065 mkvprop 7187 lt2addnq 7434 lt2mulnq 7435 ltexnqq 7438 genpdf 7538 addnqprl 7559 addnqpru 7560 addlocpr 7566 recexprlemopl 7655 caucvgsrlemgt1 7825 add4 8149 cnegex 8166 ltleadd 8434 zextle 9375 peano5uzti 9392 fnn0ind 9400 xrlttr 9827 xaddass 9901 iccshftr 10026 iccshftl 10028 iccdil 10030 icccntr 10032 fzaddel 10091 fzrev 10116 exbtwnzlemshrink 10281 xqltnle 10300 seq3val 10491 iseqf1olemab 10522 exp3vallem 10555 mulexp 10593 expadd 10596 expmul 10599 leexp1a 10609 bccl 10782 hashfacen 10851 ovshftex 10863 2shfti 10875 caucvgre 11025 cvg1nlemcau 11028 resqrexlemcvg 11063 cau3lem 11158 rexico 11265 iooinsup 11320 climmpt 11343 subcn2 11354 climrecvg1n 11391 climcvg1nlem 11392 climcaucn 11394 mertenslem2 11579 eftlcl 11731 reeftlcl 11732 dvdsext 11896 sqoddm1div8z 11926 bezoutlemaz 12039 bezoutr1 12069 dvdslcm 12104 lcmeq0 12106 lcmcl 12107 lcmneg 12109 lcmdvds 12114 coprmgcdb 12123 dvdsprime 12157 pc2dvds 12365 prmpwdvds 12390 infpnlem1 12394 1arith 12402 resmhm 12954 resmhm2b 12956 mhmco 12957 mhmima 12958 dfgrp2 12986 mulgfng 13081 subgintm 13154 ghmmhmb 13210 resghm 13216 islmod 13624 islmodd 13626 cnco 14198 cnss1 14203 tx2cn 14247 upxp 14249 metss 14471 txmetcnp 14495 cncfss 14547 cosz12 14678 bj-findis 15209 |
Copyright terms: Public domain | W3C validator |