Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ibar | Structured version Visualization version GIF version |
Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) |
Ref | Expression |
---|---|
ibar | ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2 462 | . 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | |
2 | simpr 476 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
3 | 1, 2 | impbid1 214 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 |
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 df-an 385 |
This theorem is referenced by: biantrur 526 biantrurd 528 anclb 568 pm5.42 569 anabs5 847 pm5.33 918 bianabs 920 baib 942 baibd 946 pclem6 967 moanim 2517 euan 2518 eueq3 3348 reu6 3362 ifan 4084 dfopif 4337 reusv2lem5 4799 fvopab3g 6187 riota1a 6530 dfom2 6959 suppssr 7213 mpt2curryd 7282 boxcutc 7837 funisfsupp 8163 dfac3 8827 eluz2 11569 elixx3g 12059 elfz2 12204 zmodid2 12560 shftfib 13660 dvdsssfz1 14878 modremain 14970 sadadd2lem2 15010 smumullem 15052 issubg 17417 resgrpisgrp 17438 sscntz 17582 pgrpsubgsymgbi 17650 issubrg 18603 lindsmm 19986 mdetunilem8 20244 mdetunilem9 20245 cmpsub 21013 txcnmpt 21237 fbfinnfr 21455 elfilss 21490 fixufil 21536 ibladdlem 23392 iblabslem 23400 cusgra2v 25991 eclclwwlkn1 26359 el2wlkonotot 26400 rusgranumwlklem0 26475 eupath2lem1 26504 frgra3v 26529 pjimai 28419 chrelati 28607 tltnle 28993 metidv 29263 curf 32557 unccur 32562 cnambfre 32628 itg2addnclem2 32632 ibladdnclem 32636 iblabsnclem 32643 expdiophlem1 36606 rfovcnvf1od 37318 fsovrfovd 37323 ntrneiel2 37404 reuan 39829 odd2np1ALTV 40123 cusgruvtxb 40644 usgr0edg0rusgr 40775 rgrusgrprc 40789 eclclwwlksn1 41259 eupth2lem1 41386 isrnghm 41682 rnghmval2 41685 uzlidlring 41719 islindeps 42036 elbigo2 42144 |
Copyright terms: Public domain | W3C validator |