Metamath Proof Explorer


Theorem uun2221p1

Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis uun2221p1.1 ( ( 𝜑 ∧ ( 𝜓𝜑 ) ∧ 𝜑 ) → 𝜒 )
Assertion uun2221p1 ( ( 𝜓𝜑 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 uun2221p1.1 ( ( 𝜑 ∧ ( 𝜓𝜑 ) ∧ 𝜑 ) → 𝜒 )
2 3anrot ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) ↔ ( 𝜑 ∧ ( 𝜓𝜑 ) ∧ 𝜑 ) )
3 2 imbi1i ( ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) → 𝜒 ) ↔ ( ( 𝜑 ∧ ( 𝜓𝜑 ) ∧ 𝜑 ) → 𝜒 ) )
4 1 3 mpbir ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) → 𝜒 )
5 3anass ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) ↔ ( 𝜑 ∧ ( 𝜑 ∧ ( 𝜓𝜑 ) ) ) )
6 anabs5 ( ( 𝜑 ∧ ( 𝜑 ∧ ( 𝜓𝜑 ) ) ) ↔ ( 𝜑 ∧ ( 𝜓𝜑 ) ) )
7 5 6 bitri ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) ↔ ( 𝜑 ∧ ( 𝜓𝜑 ) ) )
8 ancom ( ( 𝜑𝜓 ) ↔ ( 𝜓𝜑 ) )
9 8 anbi2i ( ( 𝜑 ∧ ( 𝜑𝜓 ) ) ↔ ( 𝜑 ∧ ( 𝜓𝜑 ) ) )
10 7 9 bitr4i ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) ↔ ( 𝜑 ∧ ( 𝜑𝜓 ) ) )
11 anabs5 ( ( 𝜑 ∧ ( 𝜑𝜓 ) ) ↔ ( 𝜑𝜓 ) )
12 11 8 bitri ( ( 𝜑 ∧ ( 𝜑𝜓 ) ) ↔ ( 𝜓𝜑 ) )
13 10 12 bitri ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) ↔ ( 𝜓𝜑 ) )
14 13 imbi1i ( ( ( 𝜑𝜑 ∧ ( 𝜓𝜑 ) ) → 𝜒 ) ↔ ( ( 𝜓𝜑 ) → 𝜒 ) )
15 4 14 mpbi ( ( 𝜓𝜑 ) → 𝜒 )