![]() |
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 585 | 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 197 df-an 385 |
This theorem is referenced by: moeq3 3416 ssel 3630 sscon 3777 uniss 4490 trel3 4793 ssopab2 5030 coss1 5310 fununi 6002 imadif 6011 fss 6094 ssimaex 6302 ssoprab2 6753 poxp 7334 soxp 7335 pmss12g 7926 ss2ixp 7963 xpdom2 8096 fisup2g 8415 fisupcl 8416 fiinf2g 8447 inf3lem1 8563 epfrs 8645 cfub 9109 cflm 9110 fin23lem34 9206 isf32lem2 9214 axcc4 9299 domtriomlem 9302 ltexprlem3 9898 nnunb 11326 indstr 11794 qbtwnxr 12069 qsqueeze 12070 xrsupsslem 12175 xrinfmsslem 12176 ioc0 12260 climshftlem 14349 o1rlimmul 14393 ramub2 15765 monmat2matmon 20677 tgcl 20821 neips 20965 ssnei2 20968 tgcnp 21105 cnpnei 21116 cnpco 21119 hauscmplem 21257 hauscmp 21258 llyss 21330 nllyss 21331 lfinun 21376 kgen2ss 21406 txcnpi 21459 txcmplem1 21492 fgss 21724 cnpflf2 21851 fclsss1 21873 fclscf 21876 alexsubALT 21902 cnextcn 21918 tsmsxp 22005 mopni3 22346 psmetutop 22419 tngngp3 22507 iscau4 23123 caussi 23141 ovolgelb 23294 mbfi1flim 23535 ellimc3 23688 lhop1 23822 tgbtwndiff 25446 axcontlem4 25892 sspmval 27716 shmodsi 28376 atcvat4i 29384 cdj3lem2b 29424 ifeqeqx 29487 acunirnmpt 29587 xrge0infss 29653 crefss 30044 issgon 30314 cvmlift2lem12 31422 ss2mcls 31591 poseq 31878 btwndiff 32259 seglecgr12im 32342 fnessref 32477 waj-ax 32538 lukshef-ax2 32539 icorempt2 33329 finxpreclem1 33356 tan2h 33531 poimirlem31 33570 poimir 33572 mblfinlem3 33578 mblfinlem4 33579 ismblfin 33580 cvrat4 35047 athgt 35060 ps-2 35082 paddss1 35421 paddss2 35422 cdlemg33b0 36306 cdlemg33a 36311 dihjat1lem 37034 fphpdo 37698 irrapxlem2 37704 pell14qrss1234 37737 pell1qrss14 37749 acongtr 37862 ax6e2eq 39090 islptre 40169 limccog 40170 |
Copyright terms: Public domain | W3C validator |