![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > an4 | Structured version Visualization version GIF version |
Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.) |
Ref | Expression |
---|---|
an4 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anass 470 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | |
2 | an12 644 | . . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃))) | |
3 | 2 | bianass 641 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
4 | 1, 3 | bitri 275 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 |
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 398 |
This theorem is referenced by: an42 656 an4s 659 anandi 675 anandir 676 an6 1446 an33reanOLD 1485 reeanlem 3219 reu2 3688 rmo4 3693 rmo3f 3697 rmo3 3850 2reu1 3858 2reu4lem 4488 disjiun 5097 inxp 5793 xp11 6132 dfpo2 6253 fununi 6581 fun 6709 resoprab2 7480 sorpsscmpl 7676 xporderlem 8064 poxp 8065 poseq 8095 fprlem1 8236 frrlem15 9700 dfac5lem1 10066 zorn2lem6 10444 cju 12156 ixxin 13288 elfzo2 13582 xpcogend 14866 summo 15609 prodmo 15826 dfiso2 17662 issubmd 18624 gsumval3eu 19688 dvdsrtr 20088 isirred2 20139 lspsolvlem 20619 domnmuln0 20784 abvn0b 20788 unocv 21100 pf1ind 21737 ordtrest2lem 22570 lmmo 22747 ptbasin 22944 txbasval 22973 txcnp 22987 txlm 23015 tx1stc 23017 tx2ndc 23018 isfild 23225 txflf 23373 isclmp 24476 mbfi1flimlem 25103 iblcnlem1 25168 iblre 25174 iblcn 25179 logfaclbnd 26586 axcontlem4 27958 axcontlem7 27961 ocsh 30267 pjhthmo 30286 5oalem6 30643 cvnbtwn4 31273 superpos 31338 cdj3i 31425 13an22anass 31437 smatrcl 32417 ordtrest2NEWlem 32543 cusgr3cyclex 33770 lineext 34690 outsideoftr 34743 hilbert1.2 34769 lineintmo 34771 neibastop1 34860 bj-inrab 35426 isbasisrelowllem1 35855 isbasisrelowllem2 35856 ptrest 36106 poimirlem26 36133 ismblfin 36148 unirep 36201 inixp 36216 ablo4pnp 36368 keridl 36520 ispridlc 36558 anan 36713 disjecxrn 36880 coss1cnvres 36908 br1cosscnvxrn 36965 dfeldisj3 37210 antisymrelres 37254 prtlem70 37348 lcvbr3 37514 cvrnbtwn4 37770 linepsubN 38244 pmapsub 38260 pmapjoin 38344 ltrnu 38613 diblsmopel 39663 pell1234qrmulcl 41207 isdomn3 41560 ifpan23 41806 ifpidg 41837 ifpbibib 41856 uneqsn 42371 isthincd2 47132 |
Copyright terms: Public domain | W3C validator |