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 451 | 1 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anbi2ci 455 anbi12i 456 an12 551 anandi 580 pm5.53 792 pm5.75 951 3ancoma 974 3ioran 982 an6 1310 19.26-3an 1470 19.28h 1549 19.28 1550 eeeanv 1920 sb3an 1945 moanim 2087 nfrexdya 2500 r19.26-3 2594 r19.41 2619 rexcomf 2626 3reeanv 2634 cbvreu 2687 ceqsex3v 2763 rexab 2883 rexrab 2884 rmo4 2914 rmo3f 2918 reuind 2926 sbc3an 3007 rmo3 3037 ssrab 3215 rexun 3297 elin3 3308 inass 3327 unssdif 3352 indifdir 3373 difin2 3379 inrab2 3390 rabun2 3396 reuun2 3400 undif4 3466 rexdifpr 3598 rexsns 3609 rexdifsn 3702 2ralunsn 3772 iuncom4 3867 iunxiun 3941 inuni 4128 unidif0 4140 bnd2 4146 otth2 4213 copsexg 4216 copsex4g 4219 opeqsn 4224 opelopabsbALT 4231 elpwpwel 4447 suc11g 4528 rabxp 4635 opeliunxp 4653 xpundir 4655 xpiundi 4656 xpiundir 4657 brinxp2 4665 rexiunxp 4740 brres 4884 brresg 4886 dmres 4899 resiexg 4923 dminss 5012 imainss 5013 ssrnres 5040 elxp4 5085 elxp5 5086 cnvresima 5087 coundi 5099 resco 5102 imaco 5103 coiun 5107 coi1 5113 coass 5116 xpcom 5144 dffun2 5192 fncnv 5248 imadiflem 5261 imadif 5262 imainlem 5263 mptun 5313 fcnvres 5365 dff1o2 5431 dff1o3 5432 ffoss 5458 f11o 5459 brprcneu 5473 fvun2 5547 eqfnfv3 5579 respreima 5607 f1ompt 5630 fsn 5651 abrexco 5721 imaiun 5722 f1mpt 5733 dff1o6 5738 oprabid 5865 dfoprab2 5880 oprab4 5904 mpomptx 5924 opabex3d 6081 opabex3 6082 abexssex 6085 dfopab2 6149 dfoprab3s 6150 1stconst 6180 2ndconst 6181 xporderlem 6190 spc2ed 6192 f1od2 6194 brtpos2 6210 tpostpos 6223 tposmpo 6240 oviec 6598 mapsncnv 6652 dfixp 6657 domen 6708 mapsnen 6768 xpsnen 6778 xpcomco 6783 xpassen 6787 ltexpi 7269 dfmq0qs 7361 dfplq0qs 7362 enq0enq 7363 enq0ref 7365 enq0tr 7366 nqnq0pi 7370 prnmaxl 7420 prnminu 7421 suplocexprlemloc 7653 addsrpr 7677 mulsrpr 7678 suplocsrlemb 7738 addcnsr 7766 mulcnsr 7767 ltresr 7771 addvalex 7776 axprecex 7812 elnnz 9192 fnn0ind 9298 rexuz2 9510 qreccl 9571 rexrp 9603 elixx3g 9828 elfz2 9942 elfzuzb 9945 fznn 10014 elfz2nn0 10037 fznn0 10038 4fvwrd4 10065 elfzo2 10075 fzind2 10164 cvg1nlemres 10913 fsum2dlemstep 11361 modfsummod 11385 fprodseq 11510 divalgb 11847 bezoutlemmain 11916 isprm2 12028 oddpwdc 12085 ntreq0 12679 cnnei 12779 txlm 12826 blres 12981 isms2 13001 dedekindicclemicc 13157 limcrcl 13174 bdcriota 13606 bj-peano4 13678 alsconv 13797 |
Copyright terms: Public domain | W3C validator |