![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > imim1d | Structured version Visualization version GIF version |
Description: Deduction adding nested consequents. Deduction associated with imim1 83 and imim1i 63. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.) |
Ref | Expression |
---|---|
imim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
imim1d | ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | idd 24 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
3 | 1, 2 | imim12d 81 | 1 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: imim1 83 expt 170 imbi1d 333 meredith 1685 ax13b 2082 ax12v2 2165 sbequivv 2287 axc15 2387 sbequi 2451 mo3 2580 mo3OLD 2581 2mo 2678 sstr2 3828 ssralv 3885 frss 5322 fvn0ssdmfun 6614 tfi 7331 nneneq 8431 wemaplem2 8741 unxpwdom2 8782 cantnfp1lem3 8874 infxpenlem 9169 axpowndlem3 9756 indpi 10064 fzind 11827 injresinj 12908 seqcl2 13137 seqfveq2 13141 seqshft2 13145 monoord 13149 seqsplit 13152 seqid2 13165 seqhomo 13166 seqcoll 13562 rexuzre 14499 rexico 14500 limsupbnd2 14622 rlim2lt 14636 rlim3 14637 lo1le 14790 caurcvg 14815 lcmfunsnlem1 15756 coprmprod 15780 eulerthlem2 15891 ramtlecl 16108 sylow1lem1 18397 efgsrel 18531 elcls3 21295 cncls2 21485 cnntr 21487 filssufilg 22123 ufileu 22131 alexsubALTlem3 22261 tgpt0 22330 isucn2 22491 imasdsf1olem 22586 nmoleub2lem2 23323 ovolicc2lem3 23723 dyadmbllem 23803 dvnres 24131 rlimcnp 25144 xrlimcnp 25147 ftalem2 25252 bcmono 25454 2sqlem6 25600 eupth2lems 27642 mdslmd1lem1 29756 xrge0infss 30090 subfacp1lem6 31766 cvmliftlem7 31872 cvmliftlem10 31875 ss2mcls 32064 mclsax 32065 bj-exlimh 33181 bj-nfimt 33196 bj-spimt2 33297 wl-ax8clv2 34008 mettrifi 34179 diaintclN 37214 dibintclN 37323 dihintcl 37500 mapdh9a 37945 iunrelexp0 38955 imbi12VD 40046 monoordxrv 40621 smonoord 42377 ply1mulgsumlem1 43193 setrec1lem2 43544 |
Copyright terms: Public domain | W3C validator |