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  2633  rexlimdvaa  2649  issod  4409  ordsuc  4654  fcof1  5906  riota5f  5980  ovmpodf  6135  tfrlemi1  6476  eqsuptid  7160  eqinftid  7184  ordiso2  7198  addnq0mo  7630  mulnq0mo  7631  genprndl  7704  genprndu  7705  addlocpr  7719  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemfl  7792  ltexprlemfu  7794  aptiprleml  7822  caucvgprprlemexbt  7889  addsrmo  7926  mulsrmo  7927  prodge0  8997  un0addcl  9398  un0mulcl  9399  seq3fveq2  10692  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  monoord  10702  seq3split  10705  seqsplitg  10706  seqf1oglem1  10736  seq3id2  10743  seqhomog  10747  expnegzap  10790  expcanlem  10932  bcval5  10980  seq3coll  11059  wrdind  11249  wrd2ind  11250  caucvgrelemcau  11486  cau3lem  11620  reccn2ap  11819  summodclem2  11888  zsumdc  11890  fsumf1o  11896  fisumss  11898  fsumcl2lem  11904  fsumadd  11912  fisum0diag2  11953  fsummulc2  11954  mertenslem2  12042  prodmodclem2  12083  zproddc  12085  fprodseq  12089  fprodf1o  12094  prodssdc  12095  fprodssdc  12096  fprodmul  12097  dvds0lem  12307  dvdsnegb  12314  dvdssub2  12341  isprm6  12664  hashgcdeq  12757  modprminv  12767  modprminveq  12768  reumodprminv  12771  pcqmul  12821  pcqcl  12824  pcxnn0cl  12828  pcxcl  12829  pc2dvds  12848  pcadd  12858  pcmpt  12861  pockthg  12875  infpnlem1  12877  mgmidsssn0  13412  mhmeql  13520  grprcan  13565  dfgrp3mlem  13626  mulgnn0ass  13690  isnsg3  13739  ghmpreima  13798  ghmeql  13799  lss1d  14341  znidomb  14616  topssnei  14830  innei  14831  cnptopco  14890  cncnpi  14896  cncnp  14898  cnconst2  14901  cnpdis  14910  lmtopcnp  14918  tx2cn  14938  txdis  14945  blssps  15095  blss  15096  neibl  15159  metss  15162  metequiv2  15164  metrest  15174  metcnp3  15179  ivthinclemlopn  15304  ivthinclemlr  15305  ivthinclemuopn  15306  ivthinclemur  15307  ivthinclemloc  15309  plycolemc  15426  mpodvdsmulf1o  15658  perfectlem2  15668  2sqlem5  15792  2sqlem6  15793  2sqlem8  15796  2sqlem10  15798  nconstwlpolem  16392