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  2453  elabgtOLD  3606  mob2  3652  ssn0rex  4292  reusv2lem2  5325  copsex2t  5409  reuop  6200  trssord  6287  trsuc  6356  funimass2  6534  fvelima  6855  fvmptf  6916  funfvima2  7127  funfvima3  7132  tfi  7720  suppssov1  8034  tposf2  8086  frrlem4  8125  wfrlem4OLD  8163  wfrlem10OLD  8169  ectocld  8593  mapsnd  8694  resixpfo  8744  f1oeng  8781  nneneq  9017  nneneqOLD  9029  nnsdomg  9101  fiint  9119  fodomfi  9120  eqinf  9271  hartogslem1  9329  cantnf  9479  rankwflemb  9579  carden2a  9752  carduni  9767  harval2  9783  cardaleph  9873  alephval3  9894  dfac5  9912  cfcof  10058  axdc4lem  10239  nqereu  10713  recexsr  10891  seqcoll  14206  swrdswrd  14446  swrdccatin1  14466  swrdccatin2  14470  repswswrd  14525  climcau  15410  odd2np1  16078  lcmfunsnlem2lem2  16372  coprmproddvdslem  16395  dvdsprm  16436  vdwlem6  16715  imasvscafn  17276  dirref  18347  irredn1  19976  isdrngd  20044  psgnghm  20813  gsummoncoe1  21503  prdstopn  22807  cnextcn  23246  tnggrpr  23847  ovolctb  24682  dyadmbl  24792  itg1addlem4  24891  itg1addlem4OLD  24892  itg1le  24906  dvcnp2  25112  c1liplem1  25188  pserulm  25609  perfectlem2  26406  dchrisumlem2  26666  axlowdimlem16  27353  wlkv0  28046  wlkp1lem1  28069  wlkswwlksf1o  28272  wspniunwspnon  28316  trlsegvdeglem1  28612  frcond4  28662  2clwwlk2clwwlk  28742  opabssi  30981  nn0xmulclb  31122  zarclsiin  31849  cusgr3cyclex  33126  satfun  33401  fundmpss  33768  noresle  33928  bday1s  34053  nn0prpw  34540  bj-restpw  35291  bj-prmoore  35314  domalom  35603  cover2  35900  sticksstones11  40138  setindtr  40870  climxlim2lem  43421  2reuimp  44647  fvelsetpreimafv  44879  imasetpreimafvbijlemfo  44897  reupr  45014  lighneallem4  45102  proththd  45106  lincresunit3  45862