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 416 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 416 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: exp5j 446 oawordri 8165 oaordex 8173 odi 8194 pssnn 8724 alephval3 9524 dfac2b 9544 axdc4lem 9865 leexp1a 13527 wrdsymb0 13889 coprmproddvds 15995 lmodvsmmulgdi 19598 assamulgscm 20058 2ndcctbss 21991 2pthnloop 27439 wwlksnext 27598 frgrregord013 28101 atcvatlem 30089 umgr2cycllem 32284 exp5g 33548 cdleme48gfv1 37552 cdlemg6e 37638 dihord5apre 38278 dihglblem5apreN 38307 iccpartgt 43464 lmodvsmdi 44358 nn0sumshdiglemB 44608 |
Copyright terms: Public domain | W3C validator |