| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > exp4c | Structured version Visualization version GIF version | ||
| Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
| Ref | Expression |
|---|---|
| exp4c.1 | ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) |
| Ref | Expression |
|---|---|
| exp4c | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exp4c.1 | . . 3 ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) | |
| 2 | 1 | expd 415 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
| 3 | 2 | expd 415 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ 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 |
| This theorem is referenced by: exp5j 445 oawordri 8588 oaordex 8596 odi 8617 pssnn 9208 alephval3 10150 dfac2b 10171 axdc4lem 10495 leexp1a 14215 wrdsymb0 14587 coprmproddvds 16700 lmodvsmmulgdi 20895 assamulgscm 21921 2ndcctbss 23463 2pthnloop 29751 wwlksnext 29913 frgrregord013 30414 atcvatlem 32404 umgr2cycllem 35145 exp5g 36304 cdleme48gfv1 40538 cdlemg6e 40624 dihord5apre 41264 dihglblem5apreN 41293 iccpartgt 47414 lmodvsmdi 48295 nn0sumshdiglemB 48541 |
| Copyright terms: Public domain | W3C validator |