Theorem impel 506

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 407	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  equs5e  2456  elabgtOLD  3614  mob2  3661  ssn0rex  4302  reusv2lem2  5342  copsex2t  5436  reuop  6231  trssord  6319  trsuc  6388  funimass2  6567  fvelima  6891  fvmptf  6952  funfvima2  7163  funfvima3  7168  tfi  7767  suppssov1  8084  tposf2  8136  frrlem4  8175  wfrlem4OLD  8213  wfrlem10OLD  8219  ectocld  8644  mapsnd  8745  resixpfo  8795  f1oeng  8832  nneneq  9074  nneneqOLD  9086  nnsdomgOLD  9168  fiint  9189  fodomfi  9190  eqinf  9341  hartogslem1  9399  cantnf  9550  rankwflemb  9650  carden2a  9823  carduni  9838  harval2  9854  cardaleph  9946  alephval3  9967  dfac5  9985  cfcof  10131  axdc4lem  10312  nqereu  10786  recexsr  10964  seqcoll  14278  swrdswrd  14516  swrdccatin1  14536  swrdccatin2  14540  repswswrd  14595  climcau  15481  odd2np1  16149  lcmfunsnlem2lem2  16441  coprmproddvdslem  16464  dvdsprm  16505  vdwlem6  16784  imasvscafn  17345  dirref  18416  irredn1  20043  isdrngd  20121  psgnghm  20891  gsummoncoe1  21581  prdstopn  22885  cnextcn  23324  tnggrpr  23925  ovolctb  24760  dyadmbl  24870  itg1addlem4  24969  itg1addlem4OLD  24970  itg1le  24984  dvcnp2  25190  c1liplem1  25266  pserulm  25687  perfectlem2  26484  dchrisumlem2  26744  noresle  26951  bday1s  27076  axlowdimlem16  27614  wlkv0  28307  wlkp1lem1  28329  wlkswwlksf1o  28532  wspniunwspnon  28576  trlsegvdeglem1  28872  frcond4  28922  2clwwlk2clwwlk  29002  opabssi  31240  nn0xmulclb  31381  zarclsiin  32119  cusgr3cyclex  33397  satfun  33672  fundmpss  34024  nn0prpw  34608  bj-restpw  35376  bj-prmoore  35399  domalom  35688  cover2  35985  disjlem18  37075  sticksstones11  40377  setindtr  41117  ofoaid1  41333  ofoaid2  41334  naddcnfcom  41341  naddcnfass  41344  climxlim2lem  43731  2reuimp  44967  fvelsetpreimafv  45199  imasetpreimafvbijlemfo  45217  reupr  45334  lighneallem4  45422  proththd  45426  lincresunit3  46182