HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Syntax Definition wa 239
Description: Extend wff definition to include conjunction ('and').
Hypotheses
Ref Expression
wph wff ph
wps wff ps
Assertion
Ref Expression
wa wff (ph /\ ps)
See definition df-an 241 for more information.
Colors of variables: wff set class
Copyright terms: Public domain