![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad2ant2l | Structured version Visualization version GIF version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
ad2ant2.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
ad2ant2l | ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | adantrl 706 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantll 704 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 387 |
This theorem is referenced by: funcnvqp 6198 mpteqb 6560 mpt2fun 7039 soxp 7571 wfrlem4 7700 wfrlem4OLD 7701 oaass 7925 undifixp 8230 undom 8336 xpdom2 8343 tcrank 9044 inawinalem 9846 addcanpr 10203 ltsosr 10251 1re 10376 add42 10597 muladd 10807 mulsub 10818 divmuleq 11080 ltmul12a 11233 lemul12b 11234 lemul12a 11235 mulge0b 11247 qaddcl 12112 qmulcl 12114 iooshf 12564 fzass4 12696 elfzomelpfzo 12891 modid 13014 cshwleneq 13968 s2eq2seq 14088 tanaddlem 15298 fpwipodrs 17550 issubg4 17997 ghmpreima 18066 cntzsubg 18152 symgfixf1 18240 islmodd 19261 lssvsubcl 19336 lssvscl 19350 lmhmf1o 19441 pwsdiaglmhm 19452 lmimco 20587 scmatghm 20744 scmatmhm 20745 mat2pmatscmxcl 20952 fctop 21216 cctop 21218 opnneissb 21326 pnrmopn 21555 hausnei2 21565 neitx 21819 txcnmpt 21836 txrest 21843 tx1stc 21862 fbssfi 22049 opnfbas 22054 rnelfmlem 22164 alexsubALTlem3 22261 metcnp3 22753 cncfmet 23119 evth 23166 caucfil 23489 ovolun 23703 dveflem 24179 efnnfsumcl 25281 efchtdvds 25337 lgsdir2 25507 axdimuniq 26262 axcontlem2 26314 clwwlkf1 27445 frgrwopreglem5lem 27728 frgrwopreglem5ALT 27730 friendship 27831 hvsub4 28466 his35 28517 shscli 28748 5oalem2 29086 3oalem2 29094 hosub4 29244 hmops 29451 hmopm 29452 hmopco 29454 adjmul 29523 adjadd 29524 mdslmd1lem1 29756 mdslmd1lem2 29757 elmrsubrn 32016 dfon2lem6 32281 funline 32838 neibastop2lem 32943 isbasisrelowllem1 33798 isbasisrelowllem2 33799 mbfposadd 34066 itg2addnc 34073 fdc 34149 seqpo 34151 ismtyval 34207 paddss12 35957 mzpcompact2lem 38256 jm2.26 38510 fmtnofac2lem 42483 rnghmsubcsetclem2 42973 rhmsubcsetclem2 43019 rhmsubcrngclem2 43025 zlmodzxzsubm 43134 ltsubaddb 43301 ltsubsubb 43302 |
Copyright terms: Public domain | W3C validator |