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 612 | 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: darii 2665 festino 2674 baroco 2676 moeq3 3614 sbcimdv 3756 ssel 3880 sselOLD 3881 sscon 4039 uniss 4813 trel3 5154 ssopab2 5412 coss1 5709 fununi 6433 imadif 6442 fss 6540 ssimaex 6774 ssoprab2 7257 poxp 7873 soxp 7874 suppofssd 7923 pmss12g 8528 ss2ixp 8569 xpdom2 8718 fisup2g 9062 fisupcl 9063 fiinf2g 9094 inf3lem1 9221 epfrs 9325 cfub 9828 cflm 9829 fin23lem34 9925 isf32lem2 9933 axcc4 10018 domtriomlem 10021 ltexprlem3 10617 nnunb 12051 indstr 12477 qbtwnxr 12755 qsqueeze 12756 xrsupsslem 12862 xrinfmsslem 12863 ioc0 12947 climshftlem 15100 o1rlimmul 15145 ramub2 16530 monmat2matmon 21675 tgcl 21820 neips 21964 ssnei2 21967 tgcnp 22104 cnpnei 22115 cnpco 22118 hauscmplem 22257 hauscmp 22258 llyss 22330 nllyss 22331 lfinun 22376 kgen2ss 22406 txcnpi 22459 txcmplem1 22492 fgss 22724 cnpflf2 22851 fclsss1 22873 fclscf 22876 alexsubALT 22902 cnextcn 22918 tsmsxp 23006 mopni3 23346 psmetutop 23419 tngngp3 23508 iscau4 24130 caussi 24148 ovolgelb 24331 mbfi1flim 24575 ellimc3 24730 lhop1 24865 tgbtwndiff 26551 axcontlem4 27012 clwwlknonwwlknonb 28143 sspmval 28768 shmodsi 29424 atcvat4i 30432 cdj3lem2b 30472 ifeqeqx 30558 acunirnmpt 30670 xrge0infss 30757 crefss 31467 issgon 31757 cvmlift2lem12 32943 satfv1 32992 satfvsucsuc 32994 ss2mcls 33197 poseq 33482 btwndiff 34015 seglecgr12im 34098 fnessref 34232 waj-ax 34289 lukshef-ax2 34290 icorempo 35208 finxpreclem1 35246 fvineqsneq 35269 pibt2 35274 tan2h 35455 poimirlem31 35494 poimir 35496 mblfinlem3 35502 mblfinlem4 35503 ismblfin 35504 cvrat4 37143 athgt 37156 ps-2 37178 paddss1 37517 paddss2 37518 cdlemg33b0 38401 cdlemg33a 38406 dihjat1lem 39128 fphpdo 40283 irrapxlem2 40289 pell14qrss1234 40322 pell1qrss14 40334 acongtr 40444 grumnudlem 41517 ax6e2eq 41791 islptre 42778 limccog 42779 opnneilv 45818 |
Copyright terms: Public domain | W3C validator |