| 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 609 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: darii 2665 festino 2674 baroco 2676 moeq3 3718 sbcimdv 3859 ssel 3977 sscon 4143 uniss 4915 trel3 5269 axprlem4 5426 ssopab2 5551 coss1 5866 fununi 6641 imadif 6650 fss 6752 ssimaex 6994 ssoprab2 7501 poxp 8153 soxp 8154 poseq 8183 suppofssd 8228 pmss12g 8909 ss2ixp 8950 xpdom2 9107 fisup2g 9508 fisupcl 9509 fiinf2g 9540 inf3lem1 9668 epfrs 9771 cfub 10289 cflm 10290 fin23lem34 10386 isf32lem2 10394 axcc4 10479 domtriomlem 10482 ltexprlem3 11078 nnunb 12522 indstr 12958 qbtwnxr 13242 qsqueeze 13243 xrsupsslem 13349 xrinfmsslem 13350 ioc0 13434 climshftlem 15610 o1rlimmul 15655 ramub2 17052 monmat2matmon 22830 tgcl 22976 neips 23121 ssnei2 23124 tgcnp 23261 cnpnei 23272 cnpco 23275 hauscmplem 23414 hauscmp 23415 llyss 23487 nllyss 23488 lfinun 23533 kgen2ss 23563 txcnpi 23616 txcmplem1 23649 fgss 23881 cnpflf2 24008 fclsss1 24030 fclscf 24033 alexsubALT 24059 cnextcn 24075 tsmsxp 24163 mopni3 24507 psmetutop 24580 tngngp3 24677 iscau4 25313 caussi 25331 ovolgelb 25515 mbfi1flim 25758 ellimc3 25914 lhop1 26053 tgbtwndiff 28514 axcontlem4 28982 clwwlknonwwlknonb 30125 sspmval 30752 shmodsi 31408 atcvat4i 32416 cdj3lem2b 32456 ifeqeqx 32555 acunirnmpt 32669 xrge0infss 32764 constrextdg2lem 33789 crefss 33848 issgon 34124 cvmlift2lem12 35319 satfv1 35368 satfvsucsuc 35370 ss2mcls 35573 btwndiff 36028 seglecgr12im 36111 fnessref 36358 waj-ax 36415 lukshef-ax2 36416 bj-isrvec 37295 icorempo 37352 finxpreclem1 37390 fvineqsneq 37413 pibt2 37418 tan2h 37619 poimirlem31 37658 poimir 37660 mblfinlem3 37666 mblfinlem4 37667 ismblfin 37668 cvrat4 39445 athgt 39458 ps-2 39480 paddss1 39819 paddss2 39820 cdlemg33b0 40703 cdlemg33a 40708 dihjat1lem 41430 fphpdo 42828 irrapxlem2 42834 pell14qrss1234 42867 pell1qrss14 42879 acongtr 42990 ofoaid1 43371 ofoaid2 43372 fzunt 43468 fzuntd 43469 fzunt1d 43470 fzuntgd 43471 grumnudlem 44304 ax6e2eq 44577 modelaxreplem1 44995 islptre 45634 limccog 45635 grilcbri2 47971 opnneilv 48806 |
| Copyright terms: Public domain | W3C validator |