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 611 | 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: sbimdvOLD 2517 sbimdOLD 2519 darii 2750 festino 2759 baroco 2761 moeq3 3680 ssel 3937 sscon 4091 uniss 4819 trel3 5153 ssopab2 5406 coss1 5699 fununi 6402 imadif 6411 fss 6500 ssimaex 6721 ssoprab2 7196 poxp 7797 soxp 7798 suppofssd 7842 pmss12g 8408 ss2ixp 8449 xpdom2 8587 fisup2g 8908 fisupcl 8909 fiinf2g 8940 inf3lem1 9067 epfrs 9149 cfub 9648 cflm 9649 fin23lem34 9745 isf32lem2 9753 axcc4 9838 domtriomlem 9841 ltexprlem3 10437 nnunb 11871 indstr 12294 qbtwnxr 12571 qsqueeze 12572 xrsupsslem 12678 xrinfmsslem 12679 ioc0 12763 climshftlem 14910 o1rlimmul 14954 ramub2 16327 monmat2matmon 21407 tgcl 21552 neips 21696 ssnei2 21699 tgcnp 21836 cnpnei 21847 cnpco 21850 hauscmplem 21989 hauscmp 21990 llyss 22062 nllyss 22063 lfinun 22108 kgen2ss 22138 txcnpi 22191 txcmplem1 22224 fgss 22456 cnpflf2 22583 fclsss1 22605 fclscf 22608 alexsubALT 22634 cnextcn 22650 tsmsxp 22738 mopni3 23079 psmetutop 23152 tngngp3 23240 iscau4 23861 caussi 23879 ovolgelb 24062 mbfi1flim 24305 ellimc3 24460 lhop1 24595 tgbtwndiff 26278 axcontlem4 26739 clwwlknonwwlknonb 27869 sspmval 28494 shmodsi 29150 atcvat4i 30158 cdj3lem2b 30198 ifeqeqx 30283 acunirnmpt 30390 xrge0infss 30470 crefss 31123 issgon 31389 cvmlift2lem12 32568 satfv1 32617 satfvsucsuc 32619 ss2mcls 32822 poseq 33102 btwndiff 33495 seglecgr12im 33578 fnessref 33712 waj-ax 33769 lukshef-ax2 33770 icorempo 34648 finxpreclem1 34686 fvineqsneq 34709 pibt2 34714 tan2h 34927 poimirlem31 34966 poimir 34968 mblfinlem3 34974 mblfinlem4 34975 ismblfin 34976 cvrat4 36617 athgt 36630 ps-2 36652 paddss1 36991 paddss2 36992 cdlemg33b0 37875 cdlemg33a 37880 dihjat1lem 38602 fphpdo 39553 irrapxlem2 39559 pell14qrss1234 39592 pell1qrss14 39604 acongtr 39714 grumnudlem 40776 ax6e2eq 41046 islptre 42052 limccog 42053 |
Copyright terms: Public domain | W3C validator |