![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anbi1i | GIF version |
Description: Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
Ref | Expression |
---|---|
bi.aa | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
anbi1i | ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi.aa | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
3 | 2 | pm5.32ri 455 | 1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: anbi2ci 459 anbi12i 460 bianassc 470 an12 561 anandi 590 pm5.53 802 pm5.75 962 3ancoma 985 3ioran 993 an6 1321 19.26-3an 1483 19.28h 1562 19.28 1563 eeeanv 1933 sb3an 1958 moanim 2100 nfrexdya 2513 r19.26-3 2607 r19.41 2632 rexcomf 2639 3reeanv 2647 cbvreu 2701 ceqsex3v 2779 rexab 2899 rexrab 2900 rmo4 2930 rmo3f 2934 reuind 2942 sbc3an 3024 rmo3 3054 ssrab 3233 rexun 3315 elin3 3326 inass 3345 unssdif 3370 indifdir 3391 difin2 3397 inrab2 3408 rabun2 3414 reuun2 3418 undif4 3485 rexdifpr 3619 rexsns 3630 rexdifsn 3723 2ralunsn 3796 iuncom4 3891 iunxiun 3965 inuni 4152 unidif0 4164 bnd2 4170 otth2 4237 copsexg 4240 copsex4g 4243 opeqsn 4248 opelopabsbALT 4255 elpwpwel 4471 suc11g 4552 rabxp 4659 opeliunxp 4677 xpundir 4679 xpiundi 4680 xpiundir 4681 brinxp2 4689 rexiunxp 4764 brres 4908 brresg 4910 dmres 4923 resiexg 4947 dminss 5038 imainss 5039 ssrnres 5066 elxp4 5111 elxp5 5112 cnvresima 5113 coundi 5125 resco 5128 imaco 5129 coiun 5133 coi1 5139 coass 5142 xpcom 5170 dffun2 5221 fncnv 5277 imadiflem 5290 imadif 5291 imainlem 5292 mptun 5342 fcnvres 5394 dff1o2 5461 dff1o3 5462 ffoss 5488 f11o 5489 brprcneu 5503 fvun2 5578 eqfnfv3 5610 respreima 5639 f1ompt 5662 fsn 5683 abrexco 5753 imaiun 5754 f1mpt 5765 dff1o6 5770 oprabid 5900 dfoprab2 5915 oprab4 5939 mpomptx 5959 opabex3d 6115 opabex3 6116 abexssex 6119 dfopab2 6183 dfoprab3s 6184 1stconst 6215 2ndconst 6216 xporderlem 6225 spc2ed 6227 f1od2 6229 brtpos2 6245 tpostpos 6258 tposmpo 6275 oviec 6634 mapsncnv 6688 dfixp 6693 domen 6744 mapsnen 6804 xpsnen 6814 xpcomco 6819 xpassen 6823 ltexpi 7314 dfmq0qs 7406 dfplq0qs 7407 enq0enq 7408 enq0ref 7410 enq0tr 7411 nqnq0pi 7415 prnmaxl 7465 prnminu 7466 suplocexprlemloc 7698 addsrpr 7722 mulsrpr 7723 suplocsrlemb 7783 addcnsr 7811 mulcnsr 7812 ltresr 7816 addvalex 7821 axprecex 7857 elnnz 9239 fnn0ind 9345 rexuz2 9557 qreccl 9618 rexrp 9650 elixx3g 9875 elfz2 9989 elfzuzb 9992 fznn 10062 elfz2nn0 10085 fznn0 10086 4fvwrd4 10113 elfzo2 10123 fzind2 10212 cvg1nlemres 10965 fsum2dlemstep 11413 modfsummod 11437 fprodseq 11562 divalgb 11900 bezoutlemmain 11969 isprm2 12087 oddpwdc 12144 ntreq0 13265 cnnei 13365 txlm 13412 blres 13567 isms2 13587 dedekindicclemicc 13743 limcrcl 13760 bdcriota 14257 bj-peano4 14329 alsconv 14448 |
Copyright terms: Public domain | W3C validator |