Theorem exp4b 367

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)

Hypothesis

Ref	Expression
exp4b.1	⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))

Assertion

Ref	Expression
exp4b	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Proof of Theorem exp4b

Step	Hyp	Ref	Expression
1		exp4b.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏))
2	1	ex 115	. 2 ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)))
3	2	exp4a 366	1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  exp43  372  reuss2  3513  nndi  6764  mulnqprl  7942  mulnqpru  7943  distrlem5prl  7960  distrlem5pru  7961  recexprlemss1l  8009  recexprlemss1u  8010  lemul12a  9201  nnmulcl  9335  elfz0fzfz0  10550  fzo1fzo0n0  10612  fzofzim  10617  elincfzoext  10628  elfzodifsumelfzo  10636  le2sq2  11073  swrdswrd  11499  swrdccat3blem  11533  oddprmgt2  12938  infpnlem1  13167  lmodvsdi  14757