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  2458  mob2  3669  ssn0rex  4303  reusv2lem2  5332  copsex2t  5427  reuop  6235  trssord  6318  trsuc  6390  funimass2  6559  fvelima  6882  fvmptf  6945  funfvima2  7160  funfvima3  7165  tfi  7778  suppssov1  8122  suppssov2  8123  tposf2  8175  frrlem4  8214  ectocld  8701  mapsnd  8805  resixpfo  8855  f1oeng  8888  nneneq  9110  fodomfi  9191  fiint  9206  fodomfiOLD  9209  eqinf  9364  hartogslem1  9423  cantnf  9578  rankwflemb  9681  carden2a  9854  carduni  9869  harval2  9885  cardaleph  9975  alephval3  9996  dfac5  10015  cfcof  10160  axdc4lem  10341  nqereu  10815  recexsr  10993  seqcoll  14366  swrdswrd  14607  swrdccatin1  14627  swrdccatin2  14631  repswswrd  14686  climcau  15573  odd2np1  16247  lcmfunsnlem2lem2  16545  coprmproddvdslem  16568  dvdsprm  16609  vdwlem6  16893  imasvscafn  17436  dirref  18502  irredn1  20339  isdrngd  20675  isdrngdOLD  20677  psgnghm  21512  gsummoncoe1  22218  prdstopn  23538  cnextcn  23977  tnggrpr  24565  ovolctb  25413  dyadmbl  25523  itg1addlem4  25622  itg1le  25636  dvcnp2  25843  dvcnp2OLD  25844  c1liplem1  25923  pserulm  26353  fsumdvdsmul  27127  perfectlem2  27163  dchrisumlem2  27423  noresle  27631  bday1s  27770  readdscl  28396  remulscl  28399  axlowdimlem16  28930  wlkv0  29623  wlkp1lem1  29645  wlkswwlksf1o  29852  wspniunwspnon  29896  trlsegvdeglem1  30192  frcond4  30242  2clwwlk2clwwlk  30322  opabssi  32588  nn0xmulclb  32746  zarclsiin  33876  rankval4b  35103  cusgr3cyclex  35172  satfun  35447  fundmpss  35803  nn0prpw  36357  bj-restpw  37126  bj-prmoore  37149  domalom  37438  cover2  37755  disjlem18  38838  sticksstones11  42189  setindtr  43057  onov0suclim  43307  oe0suclim  43310  ofoaid1  43391  ofoaid2  43392  naddcnfcom  43399  naddcnfass  43402  omssaxinf2  45021  climxlim2lem  45883  sge0f1o  46420  2reuimp  47146  fvelsetpreimafv  47418  imasetpreimafvbijlemfo  47436  reupr  47553  lighneallem4  47641  proththd  47645  lincresunit3  48513  oppc1stflem  49319