Material implication (rule of inference)

In propositional logic, material implication is a valid rule of replacement that allows for a conditional statement to be replaced by a disjunction in which the antecedent is negated. The rule states that P implies Q is logically equivalent to not-P or Q and can replace each other in logical proofs.

Where "${\displaystyle \Leftrightarrow }$" is a metalogical symbol representing "can be replaced in a proof with."

The material implication rule may be written in sequent notation:

where ${\displaystyle \vdash }$ is a metalogical symbol meaning that ${\displaystyle (\neg P\lor Q)}$ is a syntactic consequence of ${\displaystyle (P\to Q)}$ in some logical system;

...
Wikipedia