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 178 imbi1d 343 meredith 1633 ax13b 2030 ax12v2 2169 sbequivvOLD 2326 axc15 2438 sbequiOLD 2530 sbequiALT 2592 mo3 2644 mo4 2646 2mo 2729 sstr2 3973 ssralv 4032 axprlem1 5315 axprlem2 5316 axpr 5320 frss 5516 fvn0ssdmfun 6835 tfi 7556 nneneq 8689 wemaplem2 9000 unxpwdom2 9041 cantnfp1lem3 9132 infxpenlem 9428 axpowndlem3 10010 indpi 10318 fzind 12069 injresinj 13148 seqcl2 13378 seqfveq2 13382 seqshft2 13386 monoord 13390 seqsplit 13393 seqid2 13406 seqhomo 13407 seqcoll 13812 rexuzre 14702 rexico 14703 limsupbnd2 14830 rlim2lt 14844 rlim3 14845 lo1le 14998 caurcvg 15023 lcmfunsnlem1 15971 coprmprod 15995 eulerthlem2 16109 ramtlecl 16326 sylow1lem1 18654 efgsrel 18791 elcls3 21621 cncls2 21811 cnntr 21813 filssufilg 22449 ufileu 22457 alexsubALTlem3 22587 tgpt0 22656 isucn2 22817 imasdsf1olem 22912 nmoleub2lem2 23649 ovolicc2lem3 24049 dyadmbllem 24129 dvnres 24457 rlimcnp 25471 xrlimcnp 25474 ftalem2 25579 bcmono 25781 2sqlem6 25927 eupth2lems 27945 mdslmd1lem1 30030 xrge0infss 30411 subfacp1lem6 32330 cvmliftlem7 32436 cvmliftlem10 32439 ss2mcls 32713 mclsax 32714 bj-sylget 33852 bj-nfimt 33869 bj-19.21t 33996 bj-19.37im 33999 bj-spimt2 34005 mettrifi 34915 diaintclN 38076 dibintclN 38185 dihintcl 38362 mapdh9a 38807 iunrelexp0 39927 mnuop3d 40487 imbi12VD 41087 monoordxrv 41638 smonoord 43412 ply1mulgsumlem1 44338 setrec1lem2 44689 |
Copyright terms: Public domain | W3C validator |