| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ad2ant2rl | Structured version Visualization version GIF version | ||
| Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.) |
| Ref | Expression |
|---|---|
| ad2ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
| Ref | Expression |
|---|---|
| ad2ant2rl | ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ad2ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
| 2 | 1 | adantrl 716 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
| 3 | 2 | adantlr 715 | 1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: poseq 8183 omwordri 8610 omxpenlem 9113 infxpabs 10251 domfin4 10351 isf32lem7 10399 ordpipq 10982 muladd 11695 lemul12b 12124 mulge0b 12138 qaddcl 13007 iooshf 13466 elfzomelpfzo 13810 expnegz 14137 swrdccatin1 14763 bitsshft 16512 setscom 17217 lubun 18560 grplmulf1o 19031 grpraddf1o 19032 srhmsubc 20680 lmodfopne 20898 lidl1el 21236 frlmipval 21799 en2top 22992 cnpnei 23272 kgenidm 23555 ufileu 23927 fmfnfmlem4 23965 isngp4 24625 fsumcn 24894 evth 24991 cmslssbn 25406 mbfmulc2lem 25682 itg1addlem4 25734 dgreq0 26305 cxplt3 26742 cxple3 26743 basellem4 27127 sltsolem1 27720 nodenselem7 27735 zmulscld 28383 axcontlem2 28980 umgr2edg 29226 nbumgrvtx 29363 clwwlkf1 30068 umgrhashecclwwlk 30097 frgrncvvdeqlem9 30326 frgrwopreglem5ALT 30341 numclwwlk7lem 30408 grpoidinvlem3 30525 grpoideu 30528 grporcan 30537 3oalem2 31682 hmops 32039 adjadd 32112 mdslmd4i 32352 mdexchi 32354 mdsymlem1 32422 bnj607 34930 cvxsconn 35248 tailfb 36378 lindsadd 37620 poimirlem14 37641 mblfinlem4 37667 ismblfin 37668 ismtyres 37815 ghomco 37898 rngoisocnv 37988 1idl 38033 ps-2 39480 cfsetsnfsetf1 47071 usgrgrtrirex 47917 grlictr 47975 gpgvtx0 48008 srhmsubcALTV 48241 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |