![]() |
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 704 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
3 | 2 | adantll 701 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 |
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 199 df-an 388 |
This theorem is referenced by: mpteqb 6613 omxpenlem 8414 fineqvlem 8527 marypha1lem 8692 fin23lem26 9545 axdc3lem4 9673 mulcmpblnr 10291 ltsrpr 10297 sub4 10732 muladd 10873 ltleadd 10924 divdivdiv 11142 divadddiv 11156 ltmul12a 11297 lt2mul2div 11319 xlemul1a 12497 fzrev 12786 facndiv 13463 fsumconst 15005 fprodconst 15192 isprm5 15907 acsfn2 16792 ghmeql 18152 subgdmdprd 18906 lssvsubcl 19437 lssvacl 19448 ocvin 20520 lindfmm 20673 scmatghm 20846 scmatmhm 20847 slesolinv 20993 slesolinvbi 20994 slesolex 20995 pm2mpf1lem 21106 pm2mpcoe1 21112 reftr 21826 alexsubALTlem2 22360 alexsubALTlem3 22361 blbas 22743 nmoco 23049 cncfmet 23219 cmetcaulem 23594 mbflimsup 23970 ulmdvlem3 24693 ptolemy 24785 3wlkdlem6 27694 vdn0conngrumgrv2 27725 frgrncvvdeqlem8 27840 frgrwopreglem5ALT 27856 grpoideu 28063 ipblnfi 28410 htthlem 28473 hvaddsub4 28634 bralnfn 29506 hmops 29578 hmopm 29579 adjadd 29651 opsqrlem1 29698 atomli 29940 chirredlem2 29949 atcvat3i 29954 mdsymlem5 29965 cdj1i 29991 derangenlem 32009 elmrsubrn 32293 dfon2lem6 32559 poseq 32622 sltsolem1 32707 pibt2 34145 matunitlindflem1 34335 mblfinlem1 34376 prdsbnd 34519 heibor1lem 34535 hl2at 35992 congneg 38968 jm2.26 39001 stoweidlem34 41756 fmtnofac2lem 43104 lindslinindsimp2 43891 ltsubaddb 43943 ltsubadd2b 43945 aacllem 44275 |
Copyright terms: Public domain | W3C validator |