Theorem impel 510

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

This theorem is referenced by:  equs5e  2466  mob2  3656  ssn0rex  4286  reusv2lem2  5328  copsex2t  5433  reuop  6244  trssord  6327  trsuc  6399  funimass2  6568  fvelima  6892  fvmptf  6957  funfvima2  7175  funfvima3  7180  tfi  7793  suppssov1  8137  suppssov2  8138  tposf2  8190  frrlem4  8229  ectocld  8719  mapsnd  8824  resixpfo  8874  f1oeng  8907  nneneq  9130  fodomfi  9212  fiint  9227  fodomfiOLD  9230  eqinf  9388  hartogslem1  9447  cantnf  9605  rankwflemb  9708  carden2a  9881  carduni  9896  harval2  9912  cardaleph  10002  alephval3  10023  dfac5  10042  cfcof  10187  axdc4lem  10368  nqereu  10843  recexsr  11021  seqcoll  14417  swrdswrd  14658  swrdccatin1  14678  swrdccatin2  14682  repswswrd  14737  climcau  15624  odd2np1  16301  lcmfunsnlem2lem2  16599  coprmproddvdslem  16622  dvdsprm  16664  vdwlem6  16948  imasvscafn  17492  dirref  18558  irredn1  20397  isdrngd  20737  isdrngdOLD  20739  psgnghm  21555  gsummoncoe1  22294  prdstopn  23611  cnextcn  24050  tnggrpr  24638  ovolctb  25475  dyadmbl  25585  itg1addlem4  25684  itg1le  25698  dvcnp2  25905  c1liplem1  25981  pserulm  26405  fsumdvdsmul  27176  perfectlem2  27211  dchrisumlem2  27471  noresle  27679  bday1  27824  readdscl  28509  remulscl  28512  axlowdimlem16  29044  wlkv0  29736  wlkp1lem1  29758  wlkswwlksf1o  29965  wspniunwspnon  30009  trlsegvdeglem1  30308  frcond4  30358  2clwwlk2clwwlk  30438  opabssi  32705  nn0xmulclb  32863  zarclsiin  34055  rankval4b  35281  cusgr3cyclex  35364  satfun  35639  fundmpss  35995  nn0prpw  36551  bj-restpw  37450  bj-prmoore  37473  cgsex2gd  37497  domalom  37766  cover2  38082  disjlem18  39270  sticksstones11  42641  setindtr  43469  onov0suclim  43719  oe0suclim  43722  ofoaid1  43803  ofoaid2  43804  naddcnfcom  43811  naddcnfass  43814  omssaxinf2  45432  climxlim2lem  46288  sge0f1o  46825  2reuimp  47578  fvelsetpreimafv  47862  imasetpreimafvbijlemfo  47880  reupr  47997  lighneallem4  48088  proththd  48092  lincresunit3  48972  oppc1stflem  49777