![]() |
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 526 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | |
2 | 1 | biancomd 462 | 1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: biantrurd 531 baib 534 baibd 538 bianabs 540 pm5.42 542 anclb 544 anabs5 661 annotanannot 833 pm5.33 834 pclem6 1023 moanimv 2608 moanim 2609 euan 2610 euanv 2613 ralanid 3085 rexanid 3086 r19.29 3104 rmoanid 3375 reuanid 3376 eueq3 3705 reu6 3720 reuan 3889 ifan 4577 dfopif 4869 notzfaus 5358 reusv2lem5 5397 dmopab2rex 5915 elpredg 6317 fvopab3g 6994 riota1a 7393 dfom2 7868 suppssr 8200 mpocurryd 8274 boxcutc 8960 funisfsupp 9402 dfac3 10155 eluz2 12872 elixx3g 13383 elfz2 13537 zmodid2 13911 shftfib 15070 dvdsssfz1 16313 modremain 16403 sadadd2lem2 16443 smumullem 16485 tltnle 18440 issubg 19114 resgrpisgrp 19135 sscntz 19314 pgrpsubgsymgbi 19400 qusecsub 19827 isrnghm 20417 rnghmval2 20420 issubrng 20523 issubrg 20549 lindsmm 21820 mdetunilem8 22607 mdetunilem9 22608 cmpsub 23390 txcnmpt 23614 hausdiag 23635 fbfinnfr 23831 elfilss 23866 fixufil 23912 ibladdlem 25835 iblabslem 25843 slenlt 27777 cusgruvtxb 29353 usgr0edg0rusgr 29507 rgrusgrprc 29521 rusgrnumwwlkslem 29898 eclclwwlkn1 30003 eupth2lem1 30146 pjimai 32104 chrelati 32292 bian1d 32380 metidv 33718 satfv1lem 35201 dmopab3rexdif 35244 copsex2b 36858 curf 37310 unccur 37315 cnambfre 37380 itg2addnclem2 37384 ibladdnclem 37388 iblabsnclem 37395 prjsprellsp 42299 expdiophlem1 42714 rfovcnvf1od 43706 fsovrfovd 43711 ntrneiel2 43788 odd2np1ALTV 47280 clnbupgrel 47439 dfvopnbgr2 47454 vopnbgrelself 47456 uzlidlring 47646 islindeps 47870 elbigo2 47974 |
Copyright terms: Public domain | W3C validator |