![]() |
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 714 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantlr 713 | 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: poseq 8163 omwordri 8593 omxpenlem 9098 infxpabs 10237 domfin4 10336 isf32lem7 10384 ordpipq 10967 muladd 11678 lemul12b 12104 mulge0b 12117 qaddcl 12982 iooshf 13438 elfzomelpfzo 13772 expnegz 14097 swrdccatin1 14711 bitsshft 16453 setscom 17152 lubun 18510 grplmulf1o 18977 grpraddf1o 18978 srhmsubc 20625 lmodfopne 20795 lidl1el 21134 frlmipval 21730 en2top 22932 cnpnei 23212 kgenidm 23495 ufileu 23867 fmfnfmlem4 23905 isngp4 24565 fsumcn 24832 evth 24929 cmslssbn 25344 mbfmulc2lem 25620 itg1addlem4 25672 itg1addlem4OLD 25673 dgreq0 26245 cxplt3 26679 cxple3 26680 basellem4 27061 sltsolem1 27654 nodenselem7 27669 axcontlem2 28848 umgr2edg 29094 nbumgrvtx 29231 clwwlkf1 29931 umgrhashecclwwlk 29960 frgrncvvdeqlem9 30189 frgrwopreglem5ALT 30204 numclwwlk7lem 30271 grpoidinvlem3 30388 grpoideu 30391 grporcan 30400 3oalem2 31545 hmops 31902 adjadd 31975 mdslmd4i 32215 mdexchi 32217 mdsymlem1 32285 bnj607 34678 cvxsconn 34984 tailfb 35992 lindsadd 37217 poimirlem14 37238 mblfinlem4 37264 ismblfin 37265 ismtyres 37412 ghomco 37495 rngoisocnv 37585 1idl 37630 ps-2 39081 cfsetsnfsetf1 46579 srhmsubcALTV 47573 aacllem 48420 |
Copyright terms: Public domain | W3C validator |