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

This theorem is referenced by:  equs5e  2458  elabgtOLD  3597  mob2  3645  ssn0rex  4286  reusv2lem2  5317  copsex2t  5400  reuop  6185  trssord  6268  trsuc  6335  funimass2  6501  fvelima  6817  fvmptf  6878  funfvima2  7089  funfvima3  7094  tfi  7675  suppssov1  7985  tposf2  8037  frrlem4  8076  wfrlem4OLD  8114  wfrlem10OLD  8120  ectocld  8531  mapsnd  8632  resixpfo  8682  f1oeng  8714  nneneq  8896  nnsdomg  9003  fiint  9021  fodomfi  9022  eqinf  9173  hartogslem1  9231  cantnf  9381  rankwflemb  9482  carden2a  9655  carduni  9670  harval2  9686  cardaleph  9776  alephval3  9797  dfac5  9815  cfcof  9961  axdc4lem  10142  nqereu  10616  recexsr  10794  seqcoll  14106  swrdswrd  14346  swrdccatin1  14366  swrdccatin2  14370  repswswrd  14425  climcau  15310  odd2np1  15978  lcmfunsnlem2lem2  16272  coprmproddvdslem  16295  dvdsprm  16336  vdwlem6  16615  imasvscafn  17165  dirref  18234  irredn1  19863  isdrngd  19931  psgnghm  20697  gsummoncoe1  21385  prdstopn  22687  cnextcn  23126  tnggrpr  23725  ovolctb  24559  dyadmbl  24669  itg1addlem4  24768  itg1addlem4OLD  24769  itg1le  24783  dvcnp2  24989  c1liplem1  25065  pserulm  25486  perfectlem2  26283  dchrisumlem2  26543  axlowdimlem16  27228  wlkv0  27920  wlkp1lem1  27943  wlkswwlksf1o  28145  wspniunwspnon  28189  trlsegvdeglem1  28485  frcond4  28535  2clwwlk2clwwlk  28615  opabssi  30854  nn0xmulclb  30996  zarclsiin  31723  cusgr3cyclex  32998  satfun  33273  fundmpss  33646  noresle  33827  bday1s  33952  nn0prpw  34439  bj-restpw  35190  bj-prmoore  35213  domalom  35502  cover2  35799  sticksstones11  40040  setindtr  40762  climxlim2lem  43276  2reuimp  44494  fvelsetpreimafv  44727  imasetpreimafvbijlemfo  44745  reupr  44862  lighneallem4  44950  proththd  44954  lincresunit3  45710