![]() |
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 703 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantlr 702 | 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: omwordri 7991 omxpenlem 8406 infxpabs 9424 domfin4 9523 isf32lem7 9571 ordpipq 10154 muladd 10865 lemul12b 11290 mulge0b 11303 qaddcl 12172 iooshf 12624 elfzomelpfzo 12949 expnegz 13271 bitsshft 15674 setscom 16373 lubun 17581 grplmulf1o 17950 lmodfopne 19384 lidl1el 19702 frlmipval 20615 en2top 21287 cnpnei 21566 kgenidm 21849 ufileu 22221 fmfnfmlem4 22259 isngp4 22914 fsumcn 23171 evth 23256 cmslssbn 23668 mbfmulc2lem 23941 itg1addlem4 23993 dgreq0 24548 cxplt3 24974 cxple3 24975 basellem4 25353 axcontlem2 26444 umgr2edg 26684 nbumgrvtx 26821 clwwlkf1 27561 umgrhashecclwwlk 27592 frgrncvvdeqlem9 27831 frgrwopreglem5ALT 27846 numclwwlk7lem 27936 grpoidinvlem3 28050 grpoideu 28053 grporcan 28062 3oalem2 29211 hmops 29568 adjadd 29641 mdslmd4i 29881 mdexchi 29883 mdsymlem1 29951 bnj607 31796 cvxsconn 32035 poseq 32556 sltsolem1 32641 nodenselem7 32655 tailfb 33186 lindsadd 34274 poimirlem14 34295 mblfinlem4 34321 ismblfin 34322 ismtyres 34476 ghomco 34559 rngoisocnv 34649 1idl 34694 ps-2 36007 srhmsubc 43651 srhmsubcALTV 43669 aacllem 44209 |
Copyright terms: Public domain | W3C validator |