![]() |
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 414 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 414 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: exp5j 444 oawordri 8572 oaordex 8580 odi 8601 pssnn 9198 pssnnOLD 9292 alephval3 10146 dfac2b 10166 axdc4lem 10489 leexp1a 14188 wrdsymb0 14552 coprmproddvds 16659 lmodvsmmulgdi 20869 assamulgscm 21894 2ndcctbss 23447 2pthnloop 29665 wwlksnext 29824 frgrregord013 30325 atcvatlem 32315 umgr2cycllem 34981 exp5g 36028 cdleme48gfv1 40248 cdlemg6e 40334 dihord5apre 40974 dihglblem5apreN 41003 iccpartgt 47035 lmodvsmdi 47797 nn0sumshdiglemB 48044 |
Copyright terms: Public domain | W3C validator |