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 716 | . 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
3 | 2 | adantll 714 | 1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: funcnvqp 6403 mpteqb 6794 mpofunOLD 7291 soxp 7849 wfrlem4 7987 oaass 8218 undifixp 8544 undom 8654 xpdom2 8661 tcrank 9386 inawinalem 10189 addcanpr 10546 ltsosr 10594 1re 10719 add42 10939 muladd 11150 mulsub 11161 divmuleq 11423 ltmul12a 11574 lemul12b 11575 lemul12a 11576 mulge0b 11588 qaddcl 12447 qmulcl 12449 iooshf 12900 fzass4 13036 elfzomelpfzo 13232 modid 13355 swrdccatin2 14180 pfxccatin12 14184 cshwleneq 14268 s2eq2seq 14388 tanaddlem 15611 fpwipodrs 17890 gsumsgrpccat 18120 issubg4 18416 ghmpreima 18498 cntzsubg 18585 symgfixf1 18683 islmodd 19759 lssvsubcl 19834 lssvscl 19846 lmhmf1o 19937 pwsdiaglmhm 19948 lmimco 20660 scmatghm 21284 scmatmhm 21285 mat2pmatscmxcl 21491 fctop 21755 cctop 21757 opnneissb 21865 pnrmopn 22094 hausnei2 22104 neitx 22358 txcnmpt 22375 txrest 22382 tx1stc 22401 fbssfi 22588 opnfbas 22593 rnelfmlem 22703 alexsubALTlem3 22800 metcnp3 23293 cncfmet 23661 evth 23711 caucfil 24035 ovolun 24251 dveflem 24731 efnnfsumcl 25840 efchtdvds 25896 lgsdir2 26066 axdimuniq 26859 axcontlem2 26911 clwwlkf1 27986 frgrwopreglem5lem 28257 frgrwopreglem5ALT 28259 friendship 28336 hvsub4 28972 his35 29023 shscli 29252 5oalem2 29590 3oalem2 29598 hosub4 29748 hmops 29955 hmopm 29956 hmopco 29958 adjmul 30027 adjadd 30028 mdslmd1lem1 30260 mdslmd1lem2 30261 satffunlem 32934 elmrsubrn 33053 dfon2lem6 33336 funline 34082 neibastop2lem 34187 isbasisrelowllem1 35149 isbasisrelowllem2 35150 mbfposadd 35447 itg2addnc 35454 fdc 35526 seqpo 35528 ismtyval 35581 paddss12 37456 mzpcompact2lem 40145 jm2.26 40396 fmtnofac2lem 44554 rnghmsubcsetclem2 45068 rhmsubcsetclem2 45114 rhmsubcrngclem2 45120 zlmodzxzsubm 45229 ltsubaddb 45389 ltsubsubb 45390 |
Copyright terms: Public domain | W3C validator |