Theorem impel 514

Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses

Ref	Expression
impel.1	⊢ (𝜑 → (𝜓 → 𝜒))
impel.2	⊢ (𝜃 → 𝜓)

Assertion

Ref	Expression
impel	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 ⊢ (𝜃 → 𝜓)
2		impel.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 35	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 411	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  equs5e  2490  mob2  3679  ssn0rex  4314  reusv2lem2  5372  copsex2t  5477  reuop  6296  trssord  6379  trsuc  6452  funimass2  6621  fvelima  6948  fvmptf  7013  funfvima2  7231  funfvima3  7236  tfi  7850  suppssov1  8194  suppssov2  8195  tposf2  8247  frrlem4  8287  ectocld  8781  mapsnd  8885  resixpfo  8935  f1oeng  8968  nneneq  9191  fodomfi  9273  fiint  9287  eqinf  9446  hartogslem1  9505  cantnf  9663  rankwflemb  9766  carden2a  9953  carduni  9968  harval2  9984  cardaleph  10074  alephval3  10095  dfac5  10113  cfcof  10259  axdc4lem  10440  nqereu  10915  recexsr  11093  seqcoll  14503  swrdswrd  14744  swrdccatin1  14764  swrdccatin2  14768  repswswrd  14823  climcau  15724  odd2np1  16400  lcmfunsnlem2lem2  16698  coprmproddvdslem  16721  dvdsprm  16763  vdwlem6  17047  imasvscafn  17592  dirref  18658  irredn1  20509  isdrngd  20850  isdrngdOLD  20852  psgnghm  21711  gsummoncoe1  22449  prdstopn  23766  cnextcn  24205  tnggrpr  24793  ovolctb  25630  dyadmbl  25740  itg1addlem4  25839  itg1le  25853  dvcnp2  26060  c1liplem1  26136  pserulm  26566  fsumdvdsmul  27340  perfectlem2  27375  dchrisumlem2  27635  noresle  27842  bday1  27988  readdscl  28673  remulscl  28676  axlowdimlem16  29288  wlkv0  29980  wlkp1lem1  30002  wlkswwlksf1o  30209  wspniunwspnon  30253  trlsegvdeglem1  30552  frcond4  30602  2clwwlk2clwwlk  30682  opabssi  32939  nn0xmulclb  33097  zarclsiin  34242  rankval4b  35474  cusgr3cyclex  35609  satfun  35884  fundmpss  36240  nn0prpw  36815  bj-restpw  37715  bj-prmoore  37738  cgsex2gd  37762  domalom  38031  cover2  38347  disjlem18  39533  sticksstones11  42904  setindtr  43734  onov0suclim  43984  oe0suclim  43987  ofoaid1  44068  ofoaid2  44069  naddcnfcom  44076  naddcnfass  44079  omssaxinf2  45680  climxlim2lem  46542  sge0f1o  47079  2reuimp  47835  fvelsetpreimafv  48119  imasetpreimafvbijlemfo  48137  reupr  48254  lighneallem4  48345  proththd  48349  lincresunit3  49244  oppc1stflem  50048