Theorem impl 461

Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.)

Hypothesis

Ref	Expression
impl.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
impl	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem impl

Step	Hyp	Ref	Expression
1		impl.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 423	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sbc2iedv  3815  csbie2t  3885  frinxp  5734  ordelord  6384  foco2  7109  f1ounsn  7280  frxp  8138  mpocurryd  8286  omsmolem  8666  erth  8772  unblem1  9284  unwdomg  9578  cflim2  10341  distrlem1pr  11110  uz11  12990  elpq  13103  xmulge0  13414  max0add  15477  lcmfunsnlem2lem1  16813  divgcdcoprm0  16840  cncongr1  16842  prmpwdvds  17082  imasleval  17713  issgrpd  18919  dfgrp3lem  19248  resscntz  19547  ablfac1c  20287  lbsind  21355  qsidomlem2  21637  isphld  21960  mplcoe5lem  22348  cply1mul  22614  smadiadetr  22990  chfacfisf  23172  chfacfisfcpmat  23173  chcoeffeq  23204  cayhamlem3  23205  tx1stc  23969  ioorcl  25898  coemullem  26569  xrlimcnp  27296  fsumdvdscom  27512  fsumvma  27540  cusgrres  30029  usgredgsscusgredg  30040  clwlkclwwlklem2a  30589  clwwlkext2edg  30647  frgrwopreglem5ALT  30923  frgr2wwlkeu  30928  frgr2wwlk1  30930  grpoidinvlem3  31108  htthlem  31519  atcvat4i  32999  abfmpeld  33248  ressupprn  33283  isarchi3  33748  ordtconnlem1  34556  soinfdom  35717  gonarlem  36159  fmlasucdisj  36164  funpartfun  36707  relowlssretop  38286  ltflcei  38531  neificl  38687  keridl  38966  eqvrelth  39627  cvrat4  40500  ps-2  40535  mpaaeu  44151  clcnvlem  44622  fcoresf1  48138  modlt0b  48438  iccpartiltu  48503  2pwp1prm  48673  bgoldbtbnd  48906  isuspgrimlem  48992  grimedg  49032  grimgrtri  49046  lmod0rng  49325  lincext1  49565