Theorem expr 375

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  animpimp2impd  559  reximddv  2597  rexlimdvaa  2612  issod  4350  ordsuc  4595  fcof1  5826  riota5f  5898  ovmpodf  6050  tfrlemi1  6385  eqsuptid  7056  eqinftid  7080  ordiso2  7094  addnq0mo  7507  mulnq0mo  7508  genprndl  7581  genprndu  7582  addlocpr  7596  ltexprlemm  7660  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemfl  7669  ltexprlemfu  7671  aptiprleml  7699  caucvgprprlemexbt  7766  addsrmo  7803  mulsrmo  7804  prodge0  8873  un0addcl  9273  un0mulcl  9274  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord  10556  seq3split  10559  seqsplitg  10560  seqf1oglem1  10590  seq3id2  10597  seqhomog  10601  expnegzap  10644  expcanlem  10786  bcval5  10834  seq3coll  10913  caucvgrelemcau  11124  cau3lem  11258  reccn2ap  11456  summodclem2  11525  zsumdc  11527  fsumf1o  11533  fisumss  11535  fsumcl2lem  11541  fsumadd  11549  fisum0diag2  11590  fsummulc2  11591  mertenslem2  11679  prodmodclem2  11720  zproddc  11722  fprodseq  11726  fprodf1o  11731  prodssdc  11732  fprodssdc  11733  fprodmul  11734  dvds0lem  11944  dvdsnegb  11951  dvdssub2  11978  isprm6  12285  hashgcdeq  12377  modprminv  12387  modprminveq  12388  reumodprminv  12391  pcqmul  12441  pcqcl  12444  pcxnn0cl  12448  pcxcl  12449  pc2dvds  12468  pcadd  12478  pcmpt  12481  pockthg  12495  infpnlem1  12497  mgmidsssn0  12967  mhmeql  13064  grprcan  13109  dfgrp3mlem  13170  mulgnn0ass  13228  isnsg3  13277  ghmpreima  13336  ghmeql  13337  lss1d  13879  znidomb  14146  topssnei  14330  innei  14331  cnptopco  14390  cncnpi  14396  cncnp  14398  cnconst2  14401  cnpdis  14410  lmtopcnp  14418  tx2cn  14438  txdis  14445  blssps  14595  blss  14596  neibl  14659  metss  14662  metequiv2  14664  metrest  14674  metcnp3  14679  ivthinclemlopn  14790  ivthinclemlr  14791  ivthinclemuopn  14792  ivthinclemur  14793  ivthinclemloc  14795  2sqlem5  15206  2sqlem6  15207  2sqlem8  15210  2sqlem10  15212  nconstwlpolem  15555