![]() |
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 | iba 528 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | |
2 | 1 | biancomd 464 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: biantrurd 533 baib 536 baibd 540 bianabs 542 pm5.42 544 anclb 546 anabs5 659 annotanannot 831 pm5.33 832 pclem6 1020 moanimv 2672 moanim 2673 euan 2674 euanv 2678 ralanid 3135 rexanid 3216 eueq3 3638 reu6 3651 reuan 3808 ifan 4432 dfopif 4707 notzfaus 5153 reusv2lem5 5194 dmopab2rex 5672 fvopab3g 6630 riota1a 6996 dfom2 7438 suppssr 7712 mpocurryd 7786 boxcutc 8353 funisfsupp 8684 dfac3 9393 eluz2 12099 elixx3g 12601 elfz2 12749 zmodid2 13117 shftfib 14265 dvdsssfz1 15501 modremain 15592 sadadd2lem2 15632 smumullem 15674 issubg 18033 resgrpisgrp 18054 sscntz 18197 pgrpsubgsymgbi 18266 issubrg 19225 lindsmm 20654 mdetunilem8 20912 mdetunilem9 20913 cmpsub 21692 txcnmpt 21916 hausdiag 21937 fbfinnfr 22133 elfilss 22168 fixufil 22214 ibladdlem 24103 iblabslem 24111 cusgruvtxb 26887 usgr0edg0rusgr 27040 rgrusgrprc 27054 rusgrnumwwlkslem 27435 eclclwwlkn1 27541 eupth2lem1 27685 pjimai 29644 chrelati 29832 tltnle 30323 metidv 30749 satfv1lem 32217 dmopab3rexdif 32260 slenlt 32840 curf 34401 unccur 34406 cnambfre 34471 itg2addnclem2 34475 ibladdnclem 34479 iblabsnclem 34486 prjsprellsp 38758 expdiophlem1 39103 rfovcnvf1od 39835 fsovrfovd 39840 ntrneiel2 39921 odd2np1ALTV 43321 isrnghm 43641 rnghmval2 43644 uzlidlring 43678 islindeps 43988 elbigo2 44093 |
Copyright terms: Public domain | W3C validator |