Metamath Proof Explorer
Description: Conjunction implies disjunction with one common formula (3/4).
(Contributed by BJ, 4Oct2019)


Ref 
Expression 

Assertion 
animorlr 
$${\u22a2}\left({\phi}\wedge {\psi}\right)\to \left({\chi}\vee {\phi}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

simpl 
$${\u22a2}\left({\phi}\wedge {\psi}\right)\to {\phi}$$ 
2 
1

olcd 
$${\u22a2}\left({\phi}\wedge {\psi}\right)\to \left({\chi}\vee {\phi}\right)$$ 