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  2457  mob2  3689  ssn0rex  4324  reusv2lem2  5357  copsex2t  5455  reuop  6269  trssord  6352  trsuc  6424  funimass2  6602  fvelima  6929  fvmptf  6992  funfvima2  7208  funfvima3  7213  tfi  7832  suppssov1  8179  suppssov2  8180  tposf2  8232  frrlem4  8271  ectocld  8758  mapsnd  8862  resixpfo  8912  f1oeng  8945  nneneq  9176  nnsdomgOLD  9254  fodomfi  9268  fiint  9284  fiintOLD  9285  fodomfiOLD  9288  eqinf  9443  hartogslem1  9502  cantnf  9653  rankwflemb  9753  carden2a  9926  carduni  9941  harval2  9957  cardaleph  10049  alephval3  10070  dfac5  10089  cfcof  10234  axdc4lem  10415  nqereu  10889  recexsr  11067  seqcoll  14436  swrdswrd  14677  swrdccatin1  14697  swrdccatin2  14701  repswswrd  14756  climcau  15644  odd2np1  16318  lcmfunsnlem2lem2  16616  coprmproddvdslem  16639  dvdsprm  16680  vdwlem6  16964  imasvscafn  17507  dirref  18567  irredn1  20342  isdrngd  20681  isdrngdOLD  20683  psgnghm  21496  gsummoncoe1  22202  prdstopn  23522  cnextcn  23961  tnggrpr  24550  ovolctb  25398  dyadmbl  25508  itg1addlem4  25607  itg1le  25621  dvcnp2  25828  dvcnp2OLD  25829  c1liplem1  25908  pserulm  26338  fsumdvdsmul  27112  perfectlem2  27148  dchrisumlem2  27408  noresle  27616  bday1s  27750  readdscl  28357  remulscl  28360  axlowdimlem16  28891  wlkv0  29586  wlkp1lem1  29608  wlkswwlksf1o  29816  wspniunwspnon  29860  trlsegvdeglem1  30156  frcond4  30206  2clwwlk2clwwlk  30286  opabssi  32548  nn0xmulclb  32701  zarclsiin  33868  cusgr3cyclex  35130  satfun  35405  fundmpss  35761  nn0prpw  36318  bj-restpw  37087  bj-prmoore  37110  domalom  37399  cover2  37716  disjlem18  38799  sticksstones11  42151  setindtr  43020  onov0suclim  43270  oe0suclim  43273  ofoaid1  43354  ofoaid2  43355  naddcnfcom  43362  naddcnfass  43365  omssaxinf2  44985  climxlim2lem  45850  sge0f1o  46387  2reuimp  47120  fvelsetpreimafv  47392  imasetpreimafvbijlemfo  47410  reupr  47527  lighneallem4  47615  proththd  47619  lincresunit3  48474  oppc1stflem  49280