Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > imbi2i | Structured version Visualization version GIF version |
Description: Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.) |
Ref | Expression |
---|---|
imbi2i.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
imbi2i | ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi2i.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 11 | . 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
3 | 2 | pm5.74i 259 | 1 ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: iman 439 pm4.14 600 nan 602 pm5.32 666 anidmdbi 676 imimorb 917 pm5.6 949 nannan 1443 alimex 1748 19.36v 1891 19.36 2085 sblim 2385 sban 2387 sbhb 2426 2sb6 2432 mo2v 2465 moabs 2489 eu1 2498 r2allem 2921 r3al 2924 r19.21t 2938 r19.21v 2943 ralbii 2963 r19.35 3065 reu2 3361 reu8 3369 2reu5lem3 3382 ssconb 3705 ssin 3797 difin 3823 reldisj 3972 ssundif 4004 raldifsni 4265 pwpw0 4284 pwsnALT 4367 unissb 4405 moabex 4854 dffr2 5003 dfepfr 5023 ssrelOLD 5131 ssrel2 5133 dffr3 5417 dffr4 5613 fncnv 5876 fun11 5877 dff13 6416 marypha2lem3 8226 dfsup2 8233 wemapsolem 8338 inf2 8403 axinf2 8420 aceq1 8823 aceq0 8824 kmlem14 8868 dfackm 8871 zfac 9165 ac6n 9190 zfcndrep 9315 zfcndac 9320 axgroth6 9529 axgroth4 9533 grothprim 9535 prime 11334 raluz2 11613 fsuppmapnn0ub 12657 mptnn0fsuppr 12661 brtrclfv 13591 rpnnen2lem12 14793 isprm2 15233 isprm4 15235 pgpfac1 18302 pgpfac 18306 isirred2 18524 pmatcollpw2lem 20401 isclo2 20702 lmres 20914 ist1-2 20961 is1stc2 21055 alexsubALTlem3 21663 itg2cn 23336 ellimc3 23449 plydivex 23856 vieta1 23871 dchrelbas2 24762 nmobndseqi 27018 nmobndseqiALT 27019 cvnbtwn3 28531 elat2 28583 ssrelf 28805 funcnvmptOLD 28850 isarchi2 29070 archiabl 29083 esumcvgre 29480 signstfvneq0 29975 bnj1098 30108 bnj1533 30176 bnj121 30194 bnj124 30195 bnj130 30198 bnj153 30204 bnj207 30205 bnj611 30242 bnj864 30246 bnj865 30247 bnj1000 30265 bnj978 30273 bnj1021 30288 bnj1047 30295 bnj1049 30296 bnj1090 30301 bnj1110 30304 bnj1128 30312 bnj1145 30315 bnj1171 30322 bnj1172 30323 bnj1174 30325 bnj1176 30327 bnj1280 30342 axinfprim 30837 dfon2lem9 30940 dffun10 31191 elicc3 31481 filnetlem4 31546 df3nandALT1 31566 df3nandALT2 31567 bj-ssbeq 31816 bj-ssb0 31817 bj-ax12ssb 31824 bj-ssbn 31830 bj-sbnf 32016 wl-nannan 32477 poimirlem30 32609 lcvnbtwn3 33333 isat3 33612 cdleme25cv 34664 cdlemefrs29bpre0 34702 cdlemk35 35218 dford4 36614 ifpidg 36855 ifpid1g 36858 ifpim23g 36859 ifpororb 36869 ifpbibib 36874 elinintrab 36902 undmrnresiss 36929 cotrintab 36940 elintima 36964 frege60b 37219 frege91 37268 frege97 37274 frege98 37275 dffrege99 37276 frege109 37286 frege110 37287 frege131 37308 frege133 37310 ntrneiiso 37409 int-rightdistd 37505 int-sqdefd 37506 int-sqgeq0d 37511 pm10.541 37588 pm13.196a 37637 2sbc6g 37638 expcomdg 37727 impexpd 37740 jcn 38228 fsummulc1f 38635 fsumiunss 38642 fnlimfvre2 38744 dvmptmulf 38827 dvmptfprodlem 38834 sge0ltfirpmpt2 39319 hoidmv1le 39484 hoidmvle 39490 vonioolem2 39572 smflimlem3 39659 rmoanim 39828 ldepslinc 42092 setrec1lem2 42234 setrec2 42241 sbidd-misc 42259 |
Copyright terms: Public domain | W3C validator |