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 451 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜃 → 𝜏))) |
3 | 2 | expd 451 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: exp5j 643 oawordri 7517 oaordex 7525 odi 7546 pssnn 8063 alephval3 8816 dfac2 8836 axdc4lem 9160 leexp1a 12781 wrdsymb0 13194 swrdnd2 13285 coprmproddvds 15215 lmodvsmmulgdi 18721 assamulgscm 19171 2ndcctbss 21068 wwlknext 26252 frgraregord013 26645 atcvatlem 28628 exp5g 31467 cdleme48gfv1 34842 cdlemg6e 34928 dihord5apre 35569 dihglblem5apreN 35598 iccpartgt 39965 2pthnloop 40937 wwlksnext 41099 av-frgraregord013 41549 lmodvsmdi 41957 lindslinindsimp1 42040 nn0sumshdiglemB 42212 |
Copyright terms: Public domain | W3C validator |