Theorem expr 372

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  animpimp2impd  548  reximddv  2533  rexlimdvaa  2548  issod  4236  ordsuc  4473  fcof1  5677  riota5f  5747  ovmpodf  5895  tfrlemi1  6222  eqsuptid  6877  eqinftid  6901  ordiso2  6913  addnq0mo  7248  mulnq0mo  7249  genprndl  7322  genprndu  7323  addlocpr  7337  ltexprlemm  7401  ltexprlemopl  7402  ltexprlemopu  7404  ltexprlemfl  7410  ltexprlemfu  7412  aptiprleml  7440  caucvgprprlemexbt  7507  addsrmo  7544  mulsrmo  7545  prodge0  8605  un0addcl  9003  un0mulcl  9004  seq3fveq2  10235  seq3shft2  10239  monoord  10242  seq3split  10245  seq3id2  10275  expnegzap  10320  expcanlem  10455  bcval5  10502  seq3coll  10578  caucvgrelemcau  10745  cau3lem  10879  reccn2ap  11075  summodclem2  11144  zsumdc  11146  fsumf1o  11152  fisumss  11154  fsumcl2lem  11160  fsumadd  11168  fisum0diag2  11209  fsummulc2  11210  mertenslem2  11298  dvds0lem  11492  dvdsnegb  11499  dvdssub2  11524  isprm6  11814  hashgcdeq  11893  topssnei  12320  innei  12321  cnptopco  12380  cncnpi  12386  cncnp  12388  cnconst2  12391  cnpdis  12400  lmtopcnp  12408  tx2cn  12428  txdis  12435  blssps  12585  blss  12586  neibl  12649  metss  12652  metequiv2  12654  metrest  12664  metcnp3  12669  ivthinclemlopn  12772  ivthinclemlr  12773  ivthinclemuopn  12774  ivthinclemur  12775  ivthinclemloc  12777