![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anbi2d | GIF version |
Description: Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
Ref | Expression |
---|---|
anbid.1 | ⊢ (φ → (ψ ↔ χ)) |
Ref | Expression |
---|---|
anbi2d | ⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anbid.1 | . . 3 ⊢ (φ → (ψ ↔ χ)) | |
2 | 1 | a1d 22 | . 2 ⊢ (φ → (θ → (ψ ↔ χ))) |
3 | 2 | pm5.32d 423 | 1 ⊢ (φ → ((θ ∧ ψ) ↔ (θ ∧ χ))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: anbi2 440 anbi12d 442 bi2anan9 538 dn1dc 866 xorbi2d 1269 dfbi3dc 1285 xordidc 1287 eleq2 2098 ceqsex2 2588 ceqsex6v 2592 vtocl2gaf 2614 ceqsrex2v 2670 mob2 2715 eqreu 2727 nelrdva 2740 psssstr 3045 undif4 3278 r19.27m 3310 ifbi 3342 preq12bg 3535 opeq2 3541 ralunsn 3559 intab 3635 opabbid 3813 opthg 3966 pocl 4031 ordelord 4084 ordtriexmid 4210 onsucsssucexmid 4212 tfisi 4253 xpeq2 4303 rabxp 4323 vtoclr 4331 opeliunxp 4338 posng 4355 opbrop 4362 rexiunxp 4421 elrnmpt1 4528 dfres2 4601 brcodir 4655 poltletr 4668 xp11m 4702 elxp4 4751 elxp5 4752 dffun4f 4861 fununi 4910 fneq2 4931 fnun 4948 feq3 4975 foeq3 5047 funfveu 5131 funbrfv 5155 ssimaexg 5178 fvopab3g 5188 fvopab3ig 5189 fvelrn 5241 fmptco 5273 fsn2 5280 elunirn 5348 isoeq2 5385 isoeq3 5386 isocnv2 5395 isoini 5400 isopolem 5404 f1oiso 5408 f1oiso2 5409 oprabbid 5500 cbvoprab3 5522 mpt2mptx 5537 mpt2fun 5545 ov 5562 ovi3 5579 ov6g 5580 ovg 5581 caoftrn 5678 f1o2ndf1 5791 xporderlem 5793 brtpos2 5807 brtposg 5810 dftpos4 5819 recseq 5862 tfrlem3-2 5868 tfrlem3-2d 5869 tfrlemi1 5887 tfrexlem 5889 freceq1 5919 freceq2 5920 frecsuc 5930 nnaordex 6036 brecop 6132 eroveu 6133 erovlem 6134 ecopovtrn 6139 ecopovtrng 6142 th3qlem1 6144 th3qlem2 6145 th3q 6147 domeng 6169 dom2lem 6188 xpcomco 6236 xpassen 6240 xpdom2 6241 ssfiexmid 6254 recexnq 6374 recmulnqg 6375 ltsonq 6382 enq0sym 6415 enq0ref 6416 enq0tr 6417 enq0breq 6419 addnq0mo 6430 mulnq0mo 6431 addnnnq0 6432 mulnnnq0 6433 elinp 6457 prdisj 6475 prarloclem3 6480 prarloc 6486 distrlem5prl 6562 distrlem5pru 6563 ltexprlemell 6572 ltexprlemelu 6573 recexprlemm 6596 addsrmo 6671 mulsrmo 6672 addsrpr 6673 mulsrpr 6674 lttrsr 6690 recexgt0sr 6701 mulgt0sr 6704 ltresr 6736 axprecex 6764 axpre-lttrn 6768 axpre-mulgt0 6771 lesub0 7269 apreap 7371 apreim 7387 zltlen 8095 prime 8113 fzind 8129 xltnegi 8518 ixxval 8535 fzval 8646 fzdifsuc 8713 elfzm11 8723 elfzo 8776 |
Copyright terms: Public domain | W3C validator |