Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > an42s | Structured version Visualization version GIF version |
Description: Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
Ref | Expression |
---|---|
an41r3s.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) |
Ref | Expression |
---|---|
an42s | ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | an41r3s.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | |
2 | 1 | an4s 865 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
3 | 2 | ancom2s 840 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ 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: nnmsucr 7592 ecopoveq 7735 sbthlem9 7963 mulclsr 9784 mulasssr 9790 distrsr 9791 ltsosr 9794 axmulf 9846 axmulass 9857 axdistr 9858 subadd4 10204 mulsub 10352 mgmidmo 17082 tgcl 20584 bwth 21023 pntibndlem2 25080 hosubadd4 28057 fdc 32711 isdrngo2 32927 unichnidl 33000 acongtr 36563 |
Copyright terms: Public domain | W3C validator |