Description: Virtual deduction proof of 3impexpbicomi . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.
h1:: | |- ( ( ph /\ ps /\ ch ) -> ( th <-> ta ) ) |
qed:1,?: e0a | |- ( ph -> ( ps -> ( ch -> ( ta <-> th ) ) ) ) |
Ref | Expression | ||
---|---|---|---|
Hypothesis | 3impexpbicomiVD.1 | ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜃 ↔ 𝜏 ) ) | |
Assertion | 3impexpbicomiVD | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜏 ↔ 𝜃 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impexpbicomiVD.1 | ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜃 ↔ 𝜏 ) ) | |
2 | 3impexpbicom | ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜃 ↔ 𝜏 ) ) ↔ ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜏 ↔ 𝜃 ) ) ) ) ) | |
3 | 2 | biimpi | ⊢ ( ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → ( 𝜃 ↔ 𝜏 ) ) → ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜏 ↔ 𝜃 ) ) ) ) ) |
4 | 1 3 | e0a | ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → ( 𝜏 ↔ 𝜃 ) ) ) ) |