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  2466  elabgtOLDOLD  3687  mob2  3737  ssn0rex  4381  reusv2lem2  5417  copsex2t  5512  reuop  6324  trssord  6412  trsuc  6482  funimass2  6661  fvelima  6987  fvmptf  7050  funfvima2  7268  funfvima3  7273  tfi  7890  suppssov1  8238  suppssov2  8239  tposf2  8291  frrlem4  8330  wfrlem4OLD  8368  wfrlem10OLD  8374  ectocld  8842  mapsnd  8944  resixpfo  8994  f1oeng  9031  nneneq  9272  nneneqOLD  9284  nnsdomgOLD  9364  fodomfi  9378  fiint  9394  fiintOLD  9395  fodomfiOLD  9398  eqinf  9553  hartogslem1  9611  cantnf  9762  rankwflemb  9862  carden2a  10035  carduni  10050  harval2  10066  cardaleph  10158  alephval3  10179  dfac5  10198  cfcof  10343  axdc4lem  10524  nqereu  10998  recexsr  11176  seqcoll  14513  swrdswrd  14753  swrdccatin1  14773  swrdccatin2  14777  repswswrd  14832  climcau  15719  odd2np1  16389  lcmfunsnlem2lem2  16686  coprmproddvdslem  16709  dvdsprm  16750  vdwlem6  17033  imasvscafn  17597  dirref  18671  irredn1  20452  isdrngd  20787  isdrngdOLD  20789  psgnghm  21621  gsummoncoe1  22333  prdstopn  23657  cnextcn  24096  tnggrpr  24697  ovolctb  25544  dyadmbl  25654  itg1addlem4  25753  itg1addlem4OLD  25754  itg1le  25768  dvcnp2  25975  dvcnp2OLD  25976  c1liplem1  26055  pserulm  26483  fsumdvdsmul  27256  perfectlem2  27292  dchrisumlem2  27552  noresle  27760  bday1s  27894  readdscl  28449  remulscl  28452  axlowdimlem16  28990  wlkv0  29687  wlkp1lem1  29709  wlkswwlksf1o  29912  wspniunwspnon  29956  trlsegvdeglem1  30252  frcond4  30302  2clwwlk2clwwlk  30382  opabssi  32635  nn0xmulclb  32778  zarclsiin  33817  cusgr3cyclex  35104  satfun  35379  fundmpss  35730  nn0prpw  36289  bj-restpw  37058  bj-prmoore  37081  domalom  37370  cover2  37675  disjlem18  38756  sticksstones11  42113  setindtr  42981  onov0suclim  43236  oe0suclim  43239  ofoaid1  43320  ofoaid2  43321  naddcnfcom  43328  naddcnfass  43331  climxlim2lem  45766  2reuimp  47030  fvelsetpreimafv  47261  imasetpreimafvbijlemfo  47279  reupr  47396  lighneallem4  47484  proththd  47488  lincresunit3  48210