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 610 | 1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 |
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 209 df-an 399 |
This theorem is referenced by: sbimdvOLD 2512 sbimdOLD 2514 darii 2748 festino 2757 baroco 2759 moeq3 3703 ssel 3961 sscon 4115 uniss 4853 trel3 5173 ssopab2 5426 coss1 5721 fununi 6424 imadif 6433 fss 6522 ssimaex 6743 ssoprab2 7216 poxp 7816 soxp 7817 suppofssd 7861 pmss12g 8427 ss2ixp 8468 xpdom2 8606 fisup2g 8926 fisupcl 8927 fiinf2g 8958 inf3lem1 9085 epfrs 9167 cfub 9665 cflm 9666 fin23lem34 9762 isf32lem2 9770 axcc4 9855 domtriomlem 9858 ltexprlem3 10454 nnunb 11887 indstr 12310 qbtwnxr 12587 qsqueeze 12588 xrsupsslem 12694 xrinfmsslem 12695 ioc0 12779 climshftlem 14925 o1rlimmul 14969 ramub2 16344 monmat2matmon 21426 tgcl 21571 neips 21715 ssnei2 21718 tgcnp 21855 cnpnei 21866 cnpco 21869 hauscmplem 22008 hauscmp 22009 llyss 22081 nllyss 22082 lfinun 22127 kgen2ss 22157 txcnpi 22210 txcmplem1 22243 fgss 22475 cnpflf2 22602 fclsss1 22624 fclscf 22627 alexsubALT 22653 cnextcn 22669 tsmsxp 22757 mopni3 23098 psmetutop 23171 tngngp3 23259 iscau4 23876 caussi 23894 ovolgelb 24075 mbfi1flim 24318 ellimc3 24471 lhop1 24605 tgbtwndiff 26286 axcontlem4 26747 clwwlknonwwlknonb 27879 sspmval 28504 shmodsi 29160 atcvat4i 30168 cdj3lem2b 30208 ifeqeqx 30291 acunirnmpt 30398 xrge0infss 30478 crefss 31108 issgon 31377 cvmlift2lem12 32556 satfv1 32605 satfvsucsuc 32607 ss2mcls 32810 poseq 33090 btwndiff 33483 seglecgr12im 33566 fnessref 33700 waj-ax 33757 lukshef-ax2 33758 icorempo 34626 finxpreclem1 34664 fvineqsneq 34687 pibt2 34692 tan2h 34878 poimirlem31 34917 poimir 34919 mblfinlem3 34925 mblfinlem4 34926 ismblfin 34927 cvrat4 36573 athgt 36586 ps-2 36608 paddss1 36947 paddss2 36948 cdlemg33b0 37831 cdlemg33a 37836 dihjat1lem 38558 fphpdo 39407 irrapxlem2 39413 pell14qrss1234 39446 pell1qrss14 39458 acongtr 39568 grumnudlem 40614 ax6e2eq 40884 islptre 41892 limccog 41893 |
Copyright terms: Public domain | W3C validator |