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:  animpimp2impd  526  reximddv  2476  rexlimdvaa  2490  issod  4146  ordsuc  4379  fcof1  5562  riota5f  5632  ovmpt2df  5776  tfrlemi1  6097  eqsuptid  6690  eqinftid  6714  ordiso2  6726  addnq0mo  7004  mulnq0mo  7005  genprndl  7078  genprndu  7079  addlocpr  7093  ltexprlemm  7157  ltexprlemopl  7158  ltexprlemopu  7160  ltexprlemfl  7166  ltexprlemfu  7168  aptiprleml  7196  caucvgprprlemexbt  7263  addsrmo  7287  mulsrmo  7288  prodge0  8313  un0addcl  8704  un0mulcl  8705  iseqfveq2  9886  seq3fveq2  9888  iseqshft2  9894  monoord  9900  seq3split  9903  iseqsplit  9904  seq3id2  9936  iseqid2  9937  expnegzap  9985  expcanlem  10120  ibcval5  10167  iseqcoll  10243  caucvgrelemcau  10409  cau3lem  10543  isummolem2  10768  zisum  10770  fsumf1o  10778  fisumss  10780  fsumcl2lem  10788  fsumadd  10796  fisum0diag2  10837  fsummulc2  10838  mertenslem2  10926  dvds0lem  11080  dvdsnegb  11087  dvdssub2  11112  isprm6  11400  hashgcdeq  11478