Theorem impel 515

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  equs5e  2488  mob2  3673  ssn0rex  4306  reusv2lem2  5361  copsex2t  5464  reuop  6295  trssord  6378  trsuc  6451  funimass2  6621  fvelima  6948  fvmptf  7013  funfvima2  7235  funfvima3  7240  tfi  7862  suppssov1  8207  suppssov2  8208  tposf2  8260  frrlem4  8300  ectocld  8796  mapsnd  8907  resixpfo  8957  f1oeng  8990  nneneq  9214  fodomfi  9297  fiint  9311  eqinf  9470  hartogslem1  9529  cantnf  9687  rankwflemb  9793  rankwflembOLD  9794  rankval4b  9873  carden2a  10040  carduni  10055  harval2  10071  cardaleph  10161  alephval3  10182  dfac5  10200  cfcof  10345  axdc4lem  10526  nqereu  11007  recexsr  11185  seqcoll  14602  swrdswrd  14847  swrdccatin1  14867  swrdccatin2  14871  repswswrd  14928  climcau  15831  odd2np1  16504  lcmfunsnlem2lem2  16807  coprmproddvdslem  16830  dvdsprm  16872  vdwlem6  17157  imasvscafn  17702  dirref  18768  irredn1  20649  isdrng5  21001  isdrngd  21015  isdrngdOLD  21017  psgnghm  21879  gsummoncoe1  22619  prdstopn  23940  cnextcn  24379  tnggrpr  24967  ovolctb  25804  dyadmbl  25914  itg1addlem4  26013  itg1le  26027  dvcnp2  26233  c1liplem1  26309  pserulm  26742  fsumdvdsmul  27515  perfectlem2  27550  dchrisumlem2  27810  noresle  28047  bday1  28193  readdscl  28878  remulscl  28881  axlowdimlem16  29528  wlkv0  30223  wlkp1lem1  30245  wlkswwlksf1o  30461  wspniunwspnon  30505  trlsegvdeglem1  30814  frcond4  30864  2clwwlk2clwwlk  30944  opabssi  33200  nn0xmulclb  33356  zarclsiin  34496  cusgr3cyclex  35890  satfun  36155  fundmpss  36511  nn0prpw  37091  bj-restpw  37993  bj-prmoore  38016  cgsex2gd  38038  domalom  38307  cover2  38629  disjlem18  39815  sticksstones11  43186  setindtr  44010  onov0suclim  44260  oe0suclim  44263  ofoaid1  44344  ofoaid2  44345  naddcnfcom  44352  naddcnfass  44355  omssaxinf2  45956  climxlim2lem  46824  sge0f1o  47361  2reuimp  48154  fvelsetpreimafv  48438  imasetpreimafvbijlemfo  48456  reupr  48573  lighneallem4  48664  proththd  48668  lincresunit3  49562  oppc1stflem  50364