Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imbi1d | GIF version |
Description: Deduction adding a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |
Ref | Expression |
---|---|
imbid.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
imbi1d | ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | biimprd 156 | . . 3 ⊢ (𝜑 → (𝜒 → 𝜓)) |
3 | 2 | imim1d 74 | . 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃))) |
4 | 1 | biimpd 142 | . . 3 ⊢ (𝜑 → (𝜓 → 𝜒)) |
5 | 4 | imim1d 74 | . 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃))) |
6 | 3, 5 | impbid 127 | 1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: imbi12d 232 imbi1 234 imim21b 250 pm5.33 573 imordc 829 drsb1 1720 ax11v2 1741 ax11v 1748 ax11ev 1749 equs5or 1751 raleqf 2545 alexeq 2721 mo2icl 2771 sbc19.21g 2882 csbiebg 2945 ralss 3060 ssuni 3623 intmin4 3664 ssexg 3917 pocl 4058 frforeq1 4098 frforeq2 4100 frind 4107 ontr2exmid 4268 elirr 4284 en2lp 4297 tfisi 4328 vtoclr 4406 sosng 4431 fun11 4986 funimass4 5245 dff13 5428 f1mpt 5431 isopolem 5481 oprabid 5557 caovcan 5685 caoftrn 5756 dfsmo2 5925 qliftfun 6211 ecoptocl 6216 ecopovtrn 6226 ecopovtrng 6229 dom2lem 6275 ssfiexmid 6361 domfiexmid 6363 findcard 6372 findcard2 6373 findcard2s 6374 supmoti 6406 eqsupti 6409 suplubti 6413 supisoex 6422 ltsonq 6588 prarloclem3 6687 lttrsr 6939 mulextsr1 6957 axpre-lttrn 7050 axpre-mulext 7054 axcaucvglemres 7065 prime 8446 raluz 8666 indstr 8681 supinfneg 8683 infsupneg 8684 fz1sbc 9113 qbtwnzlemshrink 9258 rebtwn2zlemshrink 9262 caucvgre 9867 maxleast 10099 rexanre 10106 rexico 10107 minmax 10112 addcn2 10149 mulcn2 10151 cn1lem 10152 zsupcllemstep 10341 zsupcllemex 10342 bezoutlemmain 10387 dfgcd2 10403 exprmfct 10519 prmdvdsexpr 10529 sqrt2irr 10541 pw2dvdslemn 10543 bj-rspgt 10596 bdssexg 10695 |
Copyright terms: Public domain | W3C validator |