![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > anbi12i | GIF version |
Description: Conjoin both sides of two equivalences. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
anbi12.1 | ⊢ (𝜑 ↔ 𝜓) |
anbi12.2 | ⊢ (𝜒 ↔ 𝜃) |
Ref | Expression |
---|---|
anbi12i | ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anbi12.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | anbi1i 458 | . 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
3 | anbi12.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
4 | 3 | anbi2i 457 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) |
5 | 2, 4 | bitri 184 | 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: anbi12ci 461 ordir 817 orddi 820 dcan 933 3anbi123i 1188 an6 1321 xorcom 1388 trubifal 1416 truxortru 1419 truxorfal 1420 falxortru 1421 falxorfal 1422 nford 1567 nfand 1568 sbequ8 1847 sbanv 1889 sban 1955 sbbi 1959 sbnf2 1981 eu1 2051 2exeu 2118 2eu4 2119 sbabel 2346 neanior 2434 rexeqbii 2490 r19.26m 2608 reean 2645 reu5 2689 reu2 2925 reu3 2927 eqss 3170 unss 3309 ralunb 3316 ssin 3357 undi 3383 difundi 3387 indifdir 3391 inab 3403 difab 3404 reuss2 3415 reupick 3419 raaan 3529 prss 3748 tpss 3758 prsspw 3765 prneimg 3774 uniin 3829 intun 3875 intpr 3876 disjiun 3998 brin 4055 brdif 4056 ssext 4221 pweqb 4223 opthg2 4239 copsex4g 4247 opelopabsb 4260 eqopab2b 4279 pwin 4282 pofun 4312 wetrep 4360 ordwe 4575 wessep 4577 reg3exmidlemwe 4578 elxp3 4680 soinxp 4696 relun 4743 inopab 4759 difopab 4760 inxp 4761 opelco2g 4795 cnvco 4812 dmin 4835 restidsing 4963 intasym 5013 asymref 5014 cnvdif 5035 xpm 5050 xp11m 5067 dfco2 5128 relssdmrn 5149 cnvpom 5171 xpcom 5175 dffun4 5227 dffun4f 5232 funun 5260 funcnveq 5279 fun11 5283 fununi 5284 imadif 5296 imainlem 5297 imain 5298 fnres 5332 fnopabg 5339 fun 5388 fin 5402 dff1o2 5466 brprcneu 5508 fsn 5688 dff1o6 5776 isotr 5816 brabvv 5920 eqoprab2b 5932 dfoprab3 6191 poxp 6232 cnvoprab 6234 f1od2 6235 brtpos2 6251 tfrlem7 6317 dfer2 6535 eqer 6566 iinerm 6606 brecop 6624 eroveu 6625 erovlem 6626 oviec 6640 mapval2 6677 ixpin 6722 xpcomco 6825 xpassen 6829 ssenen 6850 sbthlemi10 6964 infmoti 7026 dfmq0qs 7427 dfplq0qs 7428 enq0enq 7429 enq0tr 7432 npsspw 7469 nqprdisj 7542 ltnqpr 7591 ltnqpri 7592 ltexprlemdisj 7604 addcanprg 7614 recexprlemdisj 7628 caucvgprprlemval 7686 addsrpr 7743 mulsrpr 7744 mulgt0sr 7776 addcnsr 7832 mulcnsr 7833 ltresr 7837 addvalex 7842 axcnre 7879 axpre-suploc 7900 supinfneg 9593 infsupneg 9594 xrnemnf 9775 xrnepnf 9776 elfzuzb 10016 fzass4 10059 hashfacen 10811 rexanre 11224 cbvprod 11561 infssuzex 11944 nnwosdc 12034 isprm3 12112 issubm 12857 issubmd 12859 0subm 12865 insubm 12866 isnsg2 13056 tgval2 13482 epttop 13521 cnnei 13663 txuni2 13687 txbas 13689 txdis1cn 13709 xmeterval 13866 dedekindicc 14042 lgslem3 14334 bj-stan 14419 nnti 14664 |
Copyright terms: Public domain | W3C validator |