Theorem expr 367

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 357	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 122	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  reximddv  2464  rexlimdvaa  2478  issod  4074  ordsuc  4306  fcof1  5443  riota5f  5512  ovmpt2df  5652  tfrlemi1  5969  eqsuptid  6410  eqinftid  6434  ordiso2  6446  addnq0mo  6637  mulnq0mo  6638  genprndl  6711  genprndu  6712  addlocpr  6726  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemfl  6799  ltexprlemfu  6801  aptiprleml  6829  caucvgprprlemexbt  6896  addsrmo  6920  mulsrmo  6921  prodge0  7932  un0addcl  8321  un0mulcl  8322  iseqfveq2  9448  iseqshft2  9452  monoord  9455  iseqsplit  9458  expnegzap  9510  expcanlem  9643  ibcval5  9690  caucvgrelemcau  9866  cau3lem  10000  dvds0lem  10205  dvdsnegb  10212  dvdssub2  10237  isprm6  10526