New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > impbid1 | GIF version |
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) |
Ref | Expression |
---|---|
impbid1.1 | ⊢ (φ → (ψ → χ)) |
impbid1.2 | ⊢ (χ → ψ) |
Ref | Expression |
---|---|
impbid1 | ⊢ (φ → (ψ ↔ χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbid1.1 | . 2 ⊢ (φ → (ψ → χ)) | |
2 | impbid1.2 | . . 3 ⊢ (χ → ψ) | |
3 | 2 | a1i 10 | . 2 ⊢ (φ → (χ → ψ)) |
4 | 1, 3 | impbid 183 | 1 ⊢ (φ → (ψ ↔ χ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 |
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 177 |
This theorem is referenced by: impbid2 195 iba 489 ibar 490 pm5.71 902 cad0 1400 19.33b 1608 19.9t 1779 19.9tOLD 1857 a16gb 2050 sb4b 2054 eupickbi 2270 euor2 2272 2eu1 2284 2eu3 2286 ceqsalg 2883 undif4 3607 sneqbg 3875 adj11 3889 elpwuni 4053 opkthg 4131 iotanul 4354 preaddccan2 4455 suc11nnc 4558 phialllem1 4616 ssxpb 5055 xp11 5056 xpcan 5057 xpcan2 5058 imadif 5171 2elresin 5194 f1fveq 5473 f1elima 5474 enpw1 6062 peano4nc 6150 addceq0 6219 ce0tb 6238 addccan2nc 6265 |
Copyright terms: Public domain | W3C validator |