![]() |
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 715 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
3 | 2 | adantll 712 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: mpteqb 7020 poseq 8164 omxpenlem 9103 fineqvlem 9289 marypha1lem 9469 fin23lem26 10359 axdc3lem4 10487 mulcmpblnr 11105 ltsrpr 11111 sub4 11546 muladd 11687 ltleadd 11738 divdivdiv 11960 divadddiv 11974 ltmul12a 12115 lt2mul2div 12138 xlemul1a 13315 fzrev 13612 facndiv 14300 fsumconst 15789 fprodconst 15975 isprm5 16703 acsfn2 17671 ghmeql 19229 subgdmdprd 20030 lssvacl 20916 lssvsubcl 20917 ocvin 21666 lindfmm 21821 sraassab 21861 scmatghm 22523 scmatmhm 22524 slesolinv 22670 slesolinvbi 22671 slesolex 22672 pm2mpf1lem 22784 pm2mpcoe1 22790 reftr 23506 alexsubALTlem2 24040 alexsubALTlem3 24041 blbas 24424 nmoco 24742 cncfmet 24917 cmetcaulem 25304 mbflimsup 25683 ulmdvlem3 26428 ptolemy 26521 sltsolem1 27702 madebdaylemlrcut 27919 3wlkdlem6 30095 vdn0conngrumgrv2 30126 frgrncvvdeqlem8 30236 frgrwopreglem5ALT 30252 grpoideu 30439 ipblnfi 30785 htthlem 30847 hvaddsub4 31008 bralnfn 31878 hmops 31950 hmopm 31951 adjadd 32023 opsqrlem1 32070 atomli 32312 chirredlem2 32321 atcvat3i 32326 mdsymlem5 32337 cdj1i 32363 derangenlem 35012 elmrsubrn 35361 dfon2lem6 35625 pibt2 37137 matunitlindflem1 37330 mblfinlem1 37371 prdsbnd 37507 heibor1lem 37523 hl2at 39117 congneg 42664 jm2.26 42697 stoweidlem34 45691 fmtnofac2lem 47176 lindslinindsimp2 47882 ltsubaddb 47933 ltsubadd2b 47935 aacllem 48585 |
Copyright terms: Public domain | W3C validator |