![]() |
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 | an12 855 | . . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃))) | |
2 | 1 | anbi2i 730 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃)))) |
3 | anass 682 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | |
4 | anass 682 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃)))) | |
5 | 2, 3, 4 | 3bitr4i 292 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 |
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 197 df-an 385 |
This theorem is referenced by: an42 883 an4s 886 anandi 888 anandir 889 an6 1448 an33rean 1486 reean 3135 reu2 3427 rmo4 3432 rmo3 3561 disjiun 4672 inxp 5287 xp11 5604 fununi 6002 fun 6104 resoprab2 6799 sorpsscmpl 6990 xporderlem 7333 poxp 7334 dfac5lem1 8984 zorn2lem6 9361 cju 11054 ixxin 12230 elfzo2 12512 xpcogend 13759 summo 14492 prodmo 14710 dfiso2 16479 issubmd 17396 gsumval3eu 18351 dvdsrtr 18698 isirred2 18747 lspsolvlem 19190 domnmuln0 19346 abvn0b 19350 pf1ind 19767 unocv 20072 ordtrest2lem 21055 lmmo 21232 ptbasin 21428 txbasval 21457 txcnp 21471 txlm 21499 tx1stc 21501 tx2ndc 21502 isfild 21709 txflf 21857 isclmp 22943 mbfi1flimlem 23534 iblcnlem1 23599 iblre 23605 iblcn 23610 logfaclbnd 24992 axcontlem4 25892 axcontlem7 25895 ocsh 28270 pjhthmo 28289 5oalem6 28646 cvnbtwn4 29276 superpos 29341 cdj3i 29428 rmo3f 29462 rmo4fOLD 29463 smatrcl 29990 ordtrest2NEWlem 30096 dfpo2 31771 poseq 31878 lineext 32308 outsideoftr 32361 hilbert1.2 32387 lineintmo 32389 neibastop1 32479 bj-inrab 33048 isbasisrelowllem1 33333 isbasisrelowllem2 33334 ptrest 33538 poimirlem26 33565 ismblfin 33580 unirep 33637 inixp 33653 ablo4pnp 33809 keridl 33961 ispridlc 33999 anan 34142 br1cosscnvxrn 34364 prtlem70 34460 lcvbr3 34628 cvrnbtwn4 34884 linepsubN 35356 pmapsub 35372 pmapjoin 35456 ltrnu 35725 diblsmopel 36777 pell1234qrmulcl 37736 isdomn3 38099 ifpan23 38121 ifpidg 38153 ifpbibib 38172 uneqsn 38638 2reu1 41507 2reu4a 41510 |
Copyright terms: Public domain | W3C validator |