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 749 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
3 | 2 | adantll 746 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: reusv2lem2OLD 4796 mpteqb 6207 omxpenlem 7946 fineqvlem 8059 marypha1lem 8222 fin23lem26 9030 axdc3lem4 9158 mulcmpblnr 9771 ltsrpr 9777 sub4 10205 muladd 10341 ltleadd 10390 divdivdiv 10605 divadddiv 10619 ltmul12a 10758 lt2mul2div 10780 xlemul1a 11990 fzrev 12273 facndiv 12937 fsumconst 14364 fprodconst 14547 isprm5 15257 acsfn2 16147 ghmeql 17506 subgdmdprd 18256 lssvsubcl 18765 lssvacl 18775 ocvin 19837 lindfmm 19985 scmatghm 20158 scmatmhm 20159 slesolinv 20305 slesolinvbi 20306 slesolex 20307 pm2mpf1lem 20418 pm2mpcoe1 20424 reftr 21127 alexsubALTlem2 21662 alexsubALTlem3 21663 blbas 22045 nmoco 22351 cncfmet 22519 cmetcaulem 22894 mbflimsup 23239 ulmdvlem3 23960 ptolemy 24052 grpoideu 26747 ipblnfi 27095 htthlem 27158 hvaddsub4 27319 bralnfn 28191 hmops 28263 hmopm 28264 adjadd 28336 opsqrlem1 28383 atomli 28625 chirredlem2 28634 atcvat3i 28639 mdsymlem5 28650 cdj1i 28676 derangenlem 30407 elmrsubrn 30671 dfon2lem6 30937 poseq 30994 sltsolem1 31067 matunitlindflem1 32575 mblfinlem1 32616 prdsbnd 32762 heibor1lem 32778 hl2at 33709 congneg 36554 jm2.26 36587 stoweidlem34 38927 fmtnofac2lem 40018 31wlkdlem6 41332 vdn0conngrumgrv2 41363 lindslinindsimp2 42046 ltsubaddb 42098 ltsubadd2b 42100 aacllem 42356 |
Copyright terms: Public domain | W3C validator |