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 834 | . . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃))) | |
2 | 1 | anbi2i 726 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃)))) |
3 | anass 679 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | |
4 | anass 679 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜒 ∧ (𝜓 ∧ 𝜃)))) | |
5 | 2, 3, 4 | 3bitr4i 291 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ 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 196 df-an 385 |
This theorem is referenced by: an42 862 an4s 865 anandi 867 anandir 868 an6 1400 an33rean 1438 reean 3085 reu2 3361 rmo4 3366 rmo3 3494 disjiun 4573 inxp 5176 xp11 5488 fununi 5878 fun 5979 resoprab2 6655 sorpsscmpl 6846 xporderlem 7175 poxp 7176 dfac5lem1 8829 zorn2lem6 9206 cju 10893 ixxin 12063 elfzo2 12342 xpcogend 13561 summo 14295 prodmo 14505 dfiso2 16255 issubmd 17172 gsumval3eu 18128 dvdsrtr 18475 isirred2 18524 lspsolvlem 18963 domnmuln0 19119 abvn0b 19123 pf1ind 19540 unocv 19843 ordtrest2lem 20817 lmmo 20994 ptbasin 21190 txbasval 21219 txcnp 21233 txlm 21261 tx1stc 21263 tx2ndc 21264 isfild 21472 txflf 21620 isclmp 22705 mbfi1flimlem 23295 iblcnlem1 23360 iblre 23366 iblcn 23371 logfaclbnd 24747 axcontlem4 25647 axcontlem7 25650 ocsh 27526 pjhthmo 27545 5oalem6 27902 cvnbtwn4 28532 superpos 28597 cdj3i 28684 rmo3f 28719 rmo4fOLD 28720 smatrcl 29190 ordtrest2NEWlem 29296 dfpo2 30898 poseq 30994 lineext 31353 outsideoftr 31406 hilbert1.2 31432 lineintmo 31434 neibastop1 31524 bj-inrab 32115 isbasisrelowllem1 32379 isbasisrelowllem2 32380 ptrest 32578 poimirlem26 32605 ismblfin 32620 unirep 32677 inixp 32693 ablo4pnp 32849 keridl 33001 ispridlc 33039 prtlem70 33157 lcvbr3 33328 cvrnbtwn4 33584 linepsubN 34056 pmapsub 34072 pmapjoin 34156 ltrnu 34425 diblsmopel 35478 pell1234qrmulcl 36437 isdomn3 36801 ifpan23 36823 ifpidg 36855 ifpbibib 36874 uneqsn 37341 2reu1 39835 2reu4a 39838 |
Copyright terms: Public domain | W3C validator |