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  2463  mob2  3662  ssn0rex  4299  reusv2lem2  5336  copsex2t  5440  reuop  6251  trssord  6334  trsuc  6406  funimass2  6575  fvelima  6899  fvmptf  6963  funfvima2  7179  funfvima3  7184  tfi  7797  suppssov1  8140  suppssov2  8141  tposf2  8193  frrlem4  8232  ectocld  8722  mapsnd  8827  resixpfo  8877  f1oeng  8910  nneneq  9133  fodomfi  9215  fiint  9230  fodomfiOLD  9233  eqinf  9391  hartogslem1  9450  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  20733  isdrngdOLD  20735  psgnghm  21570  gsummoncoe1  22283  prdstopn  23603  cnextcn  24042  tnggrpr  24630  ovolctb  25467  dyadmbl  25577  itg1addlem4  25676  itg1le  25690  dvcnp2  25897  c1liplem1  25973  pserulm  26400  fsumdvdsmul  27172  perfectlem2  27207  dchrisumlem2  27467  noresle  27675  bday1  27820  readdscl  28505  remulscl  28508  axlowdimlem16  29040  wlkv0  29733  wlkp1lem1  29755  wlkswwlksf1o  29962  wspniunwspnon  30006  trlsegvdeglem1  30305  frcond4  30355  2clwwlk2clwwlk  30435  opabssi  32701  nn0xmulclb  32859  zarclsiin  34031  rankval4b  35259  cusgr3cyclex  35334  satfun  35609  fundmpss  35965  nn0prpw  36521  bj-restpw  37420  bj-prmoore  37443  cgsex2gd  37467  domalom  37734  cover2  38050  disjlem18  39238  sticksstones11  42609  setindtr  43470  onov0suclim  43720  oe0suclim  43723  ofoaid1  43804  ofoaid2  43805  naddcnfcom  43812  naddcnfass  43815  omssaxinf2  45433  climxlim2lem  46291  sge0f1o  46828  2reuimp  47575  fvelsetpreimafv  47859  imasetpreimafvbijlemfo  47877  reupr  47994  lighneallem4  48085  proththd  48089  lincresunit3  48969  oppc1stflem  49774