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 660 | . 2 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
3 | 2 | ancom2s 650 | 1 ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: nnmsucr 8353 ecopoveq 8500 sbthlem9 8764 mulclsr 10698 mulasssr 10704 distrsr 10705 ltsosr 10708 axmulf 10760 axmulass 10771 axdistr 10772 subadd4 11122 mulsub 11275 mgmidmo 18132 tgcl 21866 bwth 22307 pntibndlem2 26472 hosubadd4 29895 pibt2 35325 lindsadd 35507 fdc 35640 isdrngo2 35853 unichnidl 35926 acongtr 40503 |
Copyright terms: Public domain | W3C validator |