| 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 468 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃)))) | |
| 2 | an12 645 | . . 3 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜃))) | |
| 3 | 2 | bianass 642 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
| 4 | 1, 3 | bitri 275 | 1 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: an42 657 an4s 660 anandi 676 anandir 677 an6 1447 reeanlem 3228 reu2 3731 rmo4 3736 rmo3f 3740 rmo3 3889 2reu1 3897 2reu4lem 4522 disjiun 5131 inxp 5842 inxpOLD 5843 xp11 6195 dfpo2 6316 fununi 6641 fun 6770 resoprab2 7552 sorpsscmpl 7754 xporderlem 8152 poxp 8153 poseq 8183 fprlem1 8325 frrlem15 9797 dfac5lem1 10163 zorn2lem6 10541 cju 12262 ixxin 13404 elfzo2 13702 xpcogend 15013 summo 15753 prodmo 15972 dfiso2 17816 issubmd 18819 gsumval3eu 19922 dvdsrtr 20368 isirred2 20421 domnmuln0 20709 isdomn3 20715 abvn0b 20837 lspsolvlem 21144 unocv 21698 pf1ind 22359 ordtrest2lem 23211 lmmo 23388 ptbasin 23585 txbasval 23614 txcnp 23628 txlm 23656 tx1stc 23658 tx2ndc 23659 isfild 23866 txflf 24014 isclmp 25130 mbfi1flimlem 25757 iblcnlem1 25823 iblre 25829 iblcn 25834 logfaclbnd 27266 axcontlem4 28982 axcontlem7 28985 ocsh 31302 pjhthmo 31321 5oalem6 31678 cvnbtwn4 32308 superpos 32373 cdj3i 32460 13an22anass 32483 smatrcl 33795 ordtrest2NEWlem 33921 cusgr3cyclex 35141 lineext 36077 outsideoftr 36130 hilbert1.2 36156 lineintmo 36158 neibastop1 36360 bj-inrab 36928 isbasisrelowllem1 37356 isbasisrelowllem2 37357 ptrest 37626 poimirlem26 37653 ismblfin 37668 unirep 37721 inixp 37735 ablo4pnp 37887 keridl 38039 ispridlc 38077 anan 38230 disjecxrn 38390 coss1cnvres 38418 br1cosscnvxrn 38475 dfeldisj3 38720 antisymrelres 38764 prtlem70 38858 lcvbr3 39024 cvrnbtwn4 39280 linepsubN 39754 pmapsub 39770 pmapjoin 39854 ltrnu 40123 diblsmopel 41173 pell1234qrmulcl 42866 ifpan23 43473 ifpidg 43504 ifpbibib 43523 uneqsn 44038 isthincd2 49086 |
| Copyright terms: Public domain | W3C validator |