![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad2ant2lr | Structured version Visualization version GIF version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad2ant2lr | ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantrr 717 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
3 | 2 | adantll 714 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-an 401 |
This theorem is referenced by: mpteqb 6771 omxpenlem 8631 fineqvlem 8746 marypha1lem 8915 fin23lem26 9770 axdc3lem4 9898 mulcmpblnr 10516 ltsrpr 10522 sub4 10954 muladd 11095 ltleadd 11146 divdivdiv 11364 divadddiv 11378 ltmul12a 11519 lt2mul2div 11541 xlemul1a 12707 fzrev 13004 facndiv 13683 fsumconst 15178 fprodconst 15365 isprm5 16088 acsfn2 16977 ghmeql 18433 subgdmdprd 19209 lssvsubcl 19768 lssvacl 19779 ocvin 20424 lindfmm 20577 scmatghm 21218 scmatmhm 21219 slesolinv 21365 slesolinvbi 21366 slesolex 21367 pm2mpf1lem 21479 pm2mpcoe1 21485 reftr 22199 alexsubALTlem2 22733 alexsubALTlem3 22734 blbas 23117 nmoco 23424 cncfmet 23595 cmetcaulem 23973 mbflimsup 24351 ulmdvlem3 25081 ptolemy 25173 3wlkdlem6 28034 vdn0conngrumgrv2 28065 frgrncvvdeqlem8 28175 frgrwopreglem5ALT 28191 grpoideu 28376 ipblnfi 28722 htthlem 28784 hvaddsub4 28945 bralnfn 29815 hmops 29887 hmopm 29888 adjadd 29960 opsqrlem1 30007 atomli 30249 chirredlem2 30258 atcvat3i 30263 mdsymlem5 30274 cdj1i 30300 derangenlem 32634 elmrsubrn 32983 dfon2lem6 33265 poseq 33341 sltsolem1 33428 madebdaylemlrcut 33621 pibt2 35099 matunitlindflem1 35318 mblfinlem1 35359 prdsbnd 35496 heibor1lem 35512 hl2at 36966 congneg 40268 jm2.26 40301 stoweidlem34 43027 fmtnofac2lem 44438 lindslinindsimp2 45222 ltsubaddb 45273 ltsubadd2b 45275 aacllem 45679 |
Copyright terms: Public domain | W3C validator |