|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > simplbi2comtVD | Structured version Visualization version GIF version | ||
| Description: Virtual deduction proof of simplbi2comt 501.
     The following User's Proof is a Virtual Deduction proof completed
     automatically by the tools program completeusersproof.cmd, which invokes
     Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant.
     simplbi2comt 501 is simplbi2comtVD 44908 without virtual deductions and was
     automatically derived from simplbi2comtVD 44908. 
 | 
| Ref | Expression | 
|---|---|
| simplbi2comtVD | ⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → (𝜒 → (𝜓 → 𝜑))) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | idn1 44594 | . . . . 5 ⊢ ( (𝜑 ↔ (𝜓 ∧ 𝜒)) ▶ (𝜑 ↔ (𝜓 ∧ 𝜒)) ) | |
| 2 | biimpr 220 | . . . . 5 ⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → ((𝜓 ∧ 𝜒) → 𝜑)) | |
| 3 | 1, 2 | e1a 44647 | . . . 4 ⊢ ( (𝜑 ↔ (𝜓 ∧ 𝜒)) ▶ ((𝜓 ∧ 𝜒) → 𝜑) ) | 
| 4 | pm3.3 448 | . . . 4 ⊢ (((𝜓 ∧ 𝜒) → 𝜑) → (𝜓 → (𝜒 → 𝜑))) | |
| 5 | 3, 4 | e1a 44647 | . . 3 ⊢ ( (𝜑 ↔ (𝜓 ∧ 𝜒)) ▶ (𝜓 → (𝜒 → 𝜑)) ) | 
| 6 | pm2.04 90 | . . 3 ⊢ ((𝜓 → (𝜒 → 𝜑)) → (𝜒 → (𝜓 → 𝜑))) | |
| 7 | 5, 6 | e1a 44647 | . 2 ⊢ ( (𝜑 ↔ (𝜓 ∧ 𝜒)) ▶ (𝜒 → (𝜓 → 𝜑)) ) | 
| 8 | 7 | in1 44591 | 1 ⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → (𝜒 → (𝜓 → 𝜑))) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-vd1 44590 | 
| This theorem is referenced by: (None) | 
| Copyright terms: Public domain | W3C validator |