Theorem impel 505

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 34	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 406	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  equs5e  2460  elabgtOLDOLD  3673  mob2  3723  ssn0rex  4363  reusv2lem2  5404  copsex2t  5502  reuop  6314  trssord  6402  trsuc  6472  funimass2  6650  fvelima  6973  fvmptf  7036  funfvima2  7250  funfvima3  7255  tfi  7873  suppssov1  8220  suppssov2  8221  tposf2  8273  frrlem4  8312  wfrlem4OLD  8350  wfrlem10OLD  8356  ectocld  8822  mapsnd  8924  resixpfo  8974  f1oeng  9009  nneneq  9243  nneneqOLD  9255  nnsdomgOLD  9333  fodomfi  9347  fiint  9363  fiintOLD  9364  fodomfiOLD  9367  eqinf  9521  hartogslem1  9579  cantnf  9730  rankwflemb  9830  carden2a  10003  carduni  10018  harval2  10034  cardaleph  10126  alephval3  10147  dfac5  10166  cfcof  10311  axdc4lem  10492  nqereu  10966  recexsr  11144  seqcoll  14499  swrdswrd  14739  swrdccatin1  14759  swrdccatin2  14763  repswswrd  14818  climcau  15703  odd2np1  16374  lcmfunsnlem2lem2  16672  coprmproddvdslem  16695  dvdsprm  16736  vdwlem6  17019  imasvscafn  17583  dirref  18658  irredn1  20442  isdrngd  20781  isdrngdOLD  20783  psgnghm  21615  gsummoncoe1  22327  prdstopn  23651  cnextcn  24090  tnggrpr  24691  ovolctb  25538  dyadmbl  25648  itg1addlem4  25747  itg1addlem4OLD  25748  itg1le  25762  dvcnp2  25969  dvcnp2OLD  25970  c1liplem1  26049  pserulm  26479  fsumdvdsmul  27252  perfectlem2  27288  dchrisumlem2  27548  noresle  27756  bday1s  27890  readdscl  28445  remulscl  28448  axlowdimlem16  28986  wlkv0  29683  wlkp1lem1  29705  wlkswwlksf1o  29908  wspniunwspnon  29952  trlsegvdeglem1  30248  frcond4  30298  2clwwlk2clwwlk  30378  opabssi  32632  nn0xmulclb  32781  zarclsiin  33831  cusgr3cyclex  35120  satfun  35395  fundmpss  35747  nn0prpw  36305  bj-restpw  37074  bj-prmoore  37097  domalom  37386  cover2  37701  disjlem18  38781  sticksstones11  42137  setindtr  43012  onov0suclim  43263  oe0suclim  43266  ofoaid1  43347  ofoaid2  43348  naddcnfcom  43355  naddcnfass  43358  climxlim2lem  45800  sge0f1o  46337  2reuimp  47064  fvelsetpreimafv  47311  imasetpreimafvbijlemfo  47329  reupr  47446  lighneallem4  47534  proththd  47538  lincresunit3  48326