![]() |
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 469 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | |
2 | an12 643 | . . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃))) | |
3 | 2 | bianass 640 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
4 | 1, 3 | bitri 274 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ 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: an42 655 an4s 658 anandi 674 anandir 675 an6 1445 an33reanOLD 1484 reeanlem 3224 reu2 3717 rmo4 3722 rmo3f 3726 rmo3 3879 2reu1 3887 2reu4lem 4519 disjiun 5128 inxp 5824 xp11 6163 dfpo2 6284 fununi 6612 fun 6740 resoprab2 7511 sorpsscmpl 7707 xporderlem 8095 poxp 8096 poseq 8126 fprlem1 8267 frrlem15 9734 dfac5lem1 10100 zorn2lem6 10478 cju 12190 ixxin 13323 elfzo2 13617 xpcogend 14903 summo 15645 prodmo 15862 dfiso2 17701 issubmd 18663 gsumval3eu 19731 dvdsrtr 20134 isirred2 20185 lspsolvlem 20704 domnmuln0 20850 abvn0b 20854 unocv 21166 pf1ind 21803 ordtrest2lem 22636 lmmo 22813 ptbasin 23010 txbasval 23039 txcnp 23053 txlm 23081 tx1stc 23083 tx2ndc 23084 isfild 23291 txflf 23439 isclmp 24542 mbfi1flimlem 25169 iblcnlem1 25234 iblre 25240 iblcn 25245 logfaclbnd 26652 axcontlem4 28090 axcontlem7 28093 ocsh 30399 pjhthmo 30418 5oalem6 30775 cvnbtwn4 31405 superpos 31470 cdj3i 31557 13an22anass 31569 smatrcl 32607 ordtrest2NEWlem 32733 cusgr3cyclex 33958 lineext 34878 outsideoftr 34931 hilbert1.2 34957 lineintmo 34959 neibastop1 35048 bj-inrab 35611 isbasisrelowllem1 36040 isbasisrelowllem2 36041 ptrest 36291 poimirlem26 36318 ismblfin 36333 unirep 36386 inixp 36401 ablo4pnp 36553 keridl 36705 ispridlc 36743 anan 36898 disjecxrn 37064 coss1cnvres 37092 br1cosscnvxrn 37149 dfeldisj3 37394 antisymrelres 37438 prtlem70 37532 lcvbr3 37698 cvrnbtwn4 37954 linepsubN 38428 pmapsub 38444 pmapjoin 38528 ltrnu 38797 diblsmopel 39847 pell1234qrmulcl 41364 isdomn3 41717 ifpan23 41982 ifpidg 42013 ifpbibib 42032 uneqsn 42547 isthincd2 47306 |
Copyright terms: Public domain | W3C validator |