Metamath Proof Explorer
Description: Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28Jan1996) (Proof shortened by Wolf Lammen, 22Jun2022)


Ref 
Expression 

Hypothesis 
3exp.1 
$${\u22a2}\left({\phi}\wedge {\psi}\wedge {\chi}\right)\to {\theta}$$ 

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

3exp.1 
$${\u22a2}\left({\phi}\wedge {\psi}\wedge {\chi}\right)\to {\theta}$$ 
2 
1

3exp 
$${\u22a2}{\phi}\to \left({\psi}\to \left({\chi}\to {\theta}\right)\right)$$ 
3 
2

3imp31 
$${\u22a2}\left({\chi}\wedge {\psi}\wedge {\phi}\right)\to {\theta}$$ 