Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anim2d | Structured version Visualization version GIF version |
Description: Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
anim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
anim2d | ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idd 24 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
2 | anim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
3 | 1, 2 | anim12d 584 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: eleq2dOLD 2674 moeq3 3350 ssel 3562 sscon 3706 uniss 4394 trel3 4688 ssopab2 4926 coss1 5199 fununi 5878 imadif 5887 fss 5969 ssimaex 6173 ssoprab2 6609 poxp 7176 soxp 7177 pmss12g 7770 ss2ixp 7807 xpdom2 7940 fisup2g 8257 fisupcl 8258 fiinf2g 8289 inf3lem1 8408 epfrs 8490 cfub 8954 cflm 8955 fin23lem34 9051 isf32lem2 9059 axcc4 9144 domtriomlem 9147 ltexprlem3 9739 nnunb 11165 indstr 11632 qbtwnxr 11905 qsqueeze 11906 xrsupsslem 12009 xrinfmsslem 12010 ioc0 12093 climshftlem 14153 o1rlimmul 14197 ramub2 15556 monmat2matmon 20448 tgcl 20584 neips 20727 ssnei2 20730 tgcnp 20867 cnpnei 20878 cnpco 20881 hauscmplem 21019 hauscmp 21020 llyss 21092 nllyss 21093 lfinun 21138 kgen2ss 21168 txcnpi 21221 txcmplem1 21254 fgss 21487 cnpflf2 21614 fclsss1 21636 fclscf 21639 alexsubALT 21665 cnextcn 21681 tsmsxp 21768 mopni3 22109 psmetutop 22182 tngngp3 22270 iscau4 22885 caussi 22903 ovolgelb 23055 mbfi1flim 23296 ellimc3 23449 lhop1 23581 tgbtwndiff 25201 axcontlem4 25647 iswlkg 26052 sspmval 26972 shmodsi 27632 atcvat4i 28640 cdj3lem2b 28680 ifeqeqx 28745 acunirnmpt 28841 xrge0infss 28915 crefss 29244 issgon 29513 cvmlift2lem12 30550 ss2mcls 30719 poseq 30994 btwndiff 31304 seglecgr12im 31387 fnessref 31522 waj-ax 31583 lukshef-ax2 31584 icorempt2 32375 finxpreclem1 32402 tan2h 32571 poimirlem31 32610 poimir 32612 mblfinlem3 32618 mblfinlem4 32619 ismblfin 32620 cvrat4 33747 athgt 33760 ps-2 33782 paddss1 34121 paddss2 34122 cdlemg33b0 35007 cdlemg33a 35012 dihjat1lem 35735 fphpdo 36399 irrapxlem2 36405 pell14qrss1234 36438 pell1qrss14 36450 acongtr 36563 ax6e2eq 37794 islptre 38686 limccog 38687 |
Copyright terms: Public domain | W3C validator |