![]() |
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 443 | 1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: anbi2ci 447 anbi12i 448 an12 526 anandi 555 pm5.53 749 pm5.75 904 3ancoma 927 3ioran 935 an6 1253 19.26-3an 1413 19.28h 1495 19.28 1496 eeeanv 1851 sb3an 1875 moanim 2017 nfrexdya 2407 r19.26-3 2493 r19.41 2515 rexcomf 2522 3reeanv 2530 cbvreu 2581 ceqsex3v 2651 rexab 2764 rexrab 2765 rmo4 2795 reuind 2805 sbc3an 2885 rmo3 2915 ssrab 3082 rexun 3163 elin3 3174 inass 3193 unssdif 3216 indifdir 3237 difin2 3243 inrab2 3254 rabun2 3260 reuun2 3264 undif4 3323 rexsns 3451 rexdifsn 3541 2ralunsn 3611 iuncom4 3706 iunxiun 3778 inuni 3951 unidif0 3962 bnd2 3968 otth2 4025 copsexg 4028 copsex4g 4031 opeqsn 4036 opelopabsbALT 4043 suc11g 4329 rabxp 4427 opeliunxp 4442 xpundir 4444 xpiundi 4445 xpiundir 4446 brinxp2 4454 rexiunxp 4527 brres 4667 brresg 4669 dmres 4681 resiexg 4704 dminss 4789 imainss 4790 ssrnres 4814 elxp4 4859 elxp5 4860 cnvresima 4861 coundi 4873 resco 4876 imaco 4877 coiun 4881 coi1 4887 coass 4890 xpcom 4915 dffun2 4963 fncnv 5017 imadiflem 5030 imadif 5031 imainlem 5032 mptun 5081 fcnvres 5125 dff1o2 5184 dff1o3 5185 ffoss 5211 f11o 5212 brprcneu 5224 fvun2 5294 eqfnfv3 5321 respreima 5349 f1ompt 5374 fsn 5389 abrexco 5452 imaiun 5453 f1mpt 5464 dff1o6 5469 oprabid 5590 dfoprab2 5605 oprab4 5628 mpt2mptx 5648 opabex3d 5801 opabex3 5802 abexssex 5805 dfopab2 5868 dfoprab3s 5869 1stconst 5895 2ndconst 5896 xporderlem 5905 spc2ed 5907 f1od2 5909 brtpos2 5922 tpostpos 5935 tposmpt2 5952 oviec 6301 domen 6321 xpsnen 6388 xpcomco 6393 xpassen 6397 ltexpi 6666 dfmq0qs 6758 dfplq0qs 6759 enq0enq 6760 enq0ref 6762 enq0tr 6763 nqnq0pi 6767 prnmaxl 6817 prnminu 6818 addsrpr 7061 mulsrpr 7062 addcnsr 7141 mulcnsr 7142 ltresr 7146 addvalex 7151 axprecex 7185 elnnz 8519 fnn0ind 8621 rexuz2 8827 qreccl 8885 rexrp 8914 elixx3g 9077 elfz2 9189 elfzuzb 9192 fznn 9259 elfz2nn0 9282 fznn0 9283 4fvwrd4 9304 elfzo2 9314 fzind2 9402 cvg1nlemres 10097 divalgb 10557 bezoutlemmain 10619 isprm2 10731 oddpwdc 10784 bdcriota 10966 bj-peano4 11042 alsconv 11083 |
Copyright terms: Public domain | W3C validator |