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 454 | . 2 ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) |
3 | anbi12.2 | . . 3 ⊢ (𝜒 ↔ 𝜃) | |
4 | 3 | anbi2i 453 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) |
5 | 2, 4 | bitri 183 | 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: anbi12ci 457 ordir 807 orddi 810 dcan 923 3anbi123i 1177 an6 1310 xorcom 1377 trubifal 1405 truxortru 1408 truxorfal 1409 falxortru 1410 falxorfal 1411 nford 1554 nfand 1555 sbequ8 1834 sbanv 1876 sban 1942 sbbi 1946 sbnf2 1968 eu1 2038 2exeu 2105 2eu4 2106 sbabel 2333 neanior 2421 rexeqbii 2477 r19.26m 2595 reean 2632 reu5 2676 reu2 2909 reu3 2911 eqss 3152 unss 3291 ralunb 3298 ssin 3339 undi 3365 difundi 3369 indifdir 3373 inab 3385 difab 3386 reuss2 3397 reupick 3401 raaan 3510 prss 3723 tpss 3732 prsspw 3739 prneimg 3748 uniin 3803 intun 3849 intpr 3850 disjiun 3971 brin 4028 brdif 4029 ssext 4193 pweqb 4195 opthg2 4211 copsex4g 4219 opelopabsb 4232 eqopab2b 4251 pwin 4254 pofun 4284 wetrep 4332 ordwe 4547 wessep 4549 reg3exmidlemwe 4550 elxp3 4652 soinxp 4668 relun 4715 inopab 4730 difopab 4731 inxp 4732 opelco2g 4766 cnvco 4783 dmin 4806 intasym 4982 asymref 4983 cnvdif 5004 xpm 5019 xp11m 5036 dfco2 5097 relssdmrn 5118 cnvpom 5140 xpcom 5144 dffun4 5193 dffun4f 5198 funun 5226 funcnveq 5245 fun11 5249 fununi 5250 imadif 5262 imainlem 5263 imain 5264 fnres 5298 fnopabg 5305 fun 5354 fin 5368 dff1o2 5431 brprcneu 5473 fsn 5651 dff1o6 5738 isotr 5778 brabvv 5879 eqoprab2b 5891 dfoprab3 6151 poxp 6191 cnvoprab 6193 f1od2 6194 brtpos2 6210 tfrlem7 6276 dfer2 6493 eqer 6524 iinerm 6564 brecop 6582 eroveu 6583 erovlem 6584 oviec 6598 mapval2 6635 ixpin 6680 xpcomco 6783 xpassen 6787 ssenen 6808 sbthlemi10 6922 infmoti 6984 dfmq0qs 7361 dfplq0qs 7362 enq0enq 7363 enq0tr 7366 npsspw 7403 nqprdisj 7476 ltnqpr 7525 ltnqpri 7526 ltexprlemdisj 7538 addcanprg 7548 recexprlemdisj 7562 caucvgprprlemval 7620 addsrpr 7677 mulsrpr 7678 mulgt0sr 7710 addcnsr 7766 mulcnsr 7767 ltresr 7771 addvalex 7776 axcnre 7813 axpre-suploc 7834 supinfneg 9524 infsupneg 9525 xrnemnf 9704 xrnepnf 9705 elfzuzb 9945 fzass4 9987 hashfacen 10735 rexanre 11148 cbvprod 11485 infssuzex 11867 isprm3 12029 tgval2 12598 epttop 12637 cnnei 12779 txuni2 12803 txbas 12805 txdis1cn 12825 xmeterval 12982 dedekindicc 13158 bj-stan 13468 nnti 13715 |
Copyright terms: Public domain | W3C validator |