Theorem expr 357

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

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

Assertion

Ref	Expression
expr	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 347	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 115	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  rexlimdvaa  2434  issod  4056  ordsuc  4287  fcof1  5423  riota5f  5492  ovmpt2df  5632  tfrlemi1  5946  ordiso2  6357  addnq0mo  6545  mulnq0mo  6546  genprndl  6619  genprndu  6620  addlocpr  6634  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemfl  6707  ltexprlemfu  6709  aptiprleml  6737  caucvgprprlemexbt  6804  addsrmo  6828  mulsrmo  6829  prodge0  7820  un0addcl  8215  un0mulcl  8216  iseqfveq2  9228  iseqshft2  9232  monoord  9235  iseqsplit  9238  expnegzap  9289  caucvgrelemcau  9579  cau3lem  9710