![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > bi2anan9 | Structured version Visualization version GIF version |
Description: Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.) |
Ref | Expression |
---|---|
bi2an9.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
bi2an9.2 | ⊢ (𝜃 → (𝜏 ↔ 𝜂)) |
Ref | Expression |
---|---|
bi2anan9 | ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi2an9.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | bi2an9.2 | . 2 ⊢ (𝜃 → (𝜏 ↔ 𝜂)) | |
3 | pm4.38 636 | . 2 ⊢ (((𝜓 ↔ 𝜒) ∧ (𝜏 ↔ 𝜂)) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) | |
4 | 1, 2, 3 | syl2an 596 | 1 ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 397 |
This theorem is referenced by: bi2anan9r 638 rspc2gv 3587 2reu5 3714 ralprgf 4651 ralprg 4653 raltpg 4657 prssg 4777 prsspwg 4781 ssprss 4782 intprg 4940 opelopab2a 5490 opelxp 5667 eqrel 5738 eqrelrel 5751 brcog 5820 tpres 7146 dff13 7198 resoprab2 7469 ovig 7495 dfoprab4f 7980 f1o2ndf1 8046 om00el 8515 oeoe 8538 eroveu 8709 endisj 8960 infxpen 9908 dfac5lem4 10020 sornom 10171 ltsrpr 10971 axcnre 11058 axmulgt0 11187 wloglei 11645 mulge0b 11983 addltmul 12347 ltxr 12990 fzadd2 13430 sumsqeq0 14035 ccat0 14417 rlim 15336 cpnnen 16070 dvds2lem 16110 opoe 16204 omoe 16205 opeo 16206 omeo 16207 gcddvds 16342 dfgcd2 16386 pcqmul 16684 xpsfrnel2 17405 eqgval 18937 frgpuplem 19512 mpfind 21468 2ndcctbss 22757 txbasval 22908 cnmpt12 22969 cnmpt22 22976 prdsxmslem2 23836 ishtpy 24286 bcthlem1 24639 bcth 24644 volun 24860 vitali 24928 itg1addlem3 25013 rolle 25305 mumullem2 26480 lgsquadlem3 26681 lgsquad 26682 2sqlem7 26723 scutval 27090 slerec 27109 axpasch 27718 wlkson 28432 iswwlksnon 28626 wpthswwlks2on 28734 eulplig 29255 hlimi 29958 leopadd 30902 eqrelrd2 31362 cntzun 31726 isinftm 31841 finexttrb 32164 metidv 32276 satfv1 33760 satfbrsuc 33763 gonarlem 33791 satfv0fvfmla0 33810 satfv1fvfmla1 33820 altopthg 34483 altopthbg 34484 brsegle 34624 bj-imdirvallem 35582 finxpreclem3 35795 itg2addnclem3 36062 exan3 36686 exanres 36687 exanres3 36688 eqrel2 36691 brcoss 36824 brcoss3 36826 brcoels 36828 br1cossxrnres 36841 brcosscnv 36865 prtlem13 37261 dib1dim 39559 pellex 41060 prsprel 45573 uspgrsprf1 45943 uspgrsprfo 45944 |
Copyright terms: Public domain | W3C validator |