Theorem 3impia 1117

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1116	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  mopick2  2630  ceqsalt  3472  3gencl  3482  vtoclgft  3509  vtoclegft  3545  rspc6v  3600  mob2  3677  moi  3680  reupick3  4283  disjne  4408  elpr2elpr  4823  disji2  5079  disji  5080  tz7.2  5606  sofld  6140  ordintdif  6362  funopg  6520  fvun1  6918  fvopab6  6968  fveqressseq  7017  fvcofneq  7031  fprg  7093  isores3  7276  ovmpt4g  7500  ovmpos  7501  ov2gf  7502  ofrval  7629  sorpssuni  7672  sorpssint  7673  poxp  8068  poseq  8098  suppss2  8140  frrlem12  8237  smoel  8290  smoord  8295  smogt  8297  oaass  8486  oewordi  8516  oeoalem  8521  oeoelem  8523  nnawordi  8546  nnaass  8547  naddssim  8610  qsel  8730  xpdom3  8999  onsdominel  9050  mapdom3  9073  sdomdomtrfi  9125  domsdomtrfi  9126  php  9131  onomeneq  9138  fisseneq  9162  fodomfir  9237  cantnflem1  9604  ttrclss  9635  cfslbn  10180  cfsmolem  10183  cfcoflem  10185  infpssrlem4  10219  fin23lem7  10229  fin23lem25  10237  isf34lem7  10292  hsmexlem2  10340  axcc3  10351  axdc4lem  10368  tskss  10671  gruss  10709  gruurn  10711  gruiun  10712  gruel  10716  gruen  10725  grudomon  10730  grothac  10743  axpre-sup  11082  axsup  11210  addn0nid  11559  letrp1  11987  p1le  11988  lemul1a  11997  infrelb  12129  zextle  12568  zextlt  12569  btwnnz  12571  gtndiv  12572  uzind2  12588  fzind  12593  eluzsubOLD  12790  zsupss  12857  xrltne  13084  lemaxle  13116  qbtwnre  13120  qbtwnxr  13121  xlemul1a  13209  icogelb  13318  iccleub  13323  iccsplit  13407  uzsubsubfz  13468  elfz0fzfz0  13555  difelfznle  13564  fvffz0  13568  elfzo0le  13625  fzonmapblen  13630  fzofzim  13631  ceile  13772  modadd1  13831  muladdmodid  13836  modmul1  13850  modirr  13868  fsuppmapnn0fiub0  13919  expcl2lem  13999  expclzlem  14009  expnegz  14022  leexp2r  14100  bcval4  14233  bccmpl  14235  hashbnd  14262  hashunsnggt  14320  hashgt23el  14350  hashfundm  14368  elovmpowrd  14484  ccatval2  14504  ccatrcl1  14520  wrdl1s1  14540  ccat2s1fvw  14564  swrdsb0eq  14589  swrdccatin1  14650  pfxccatpfx2  14662  repswswrd  14709  cshwcsh2id  14754  absexpz  15231  climbdd  15598  iseraltlem2  15609  binomfallfac  15967  dvdsle  16240  divalgb  16334  ndvdssub  16339  dvdsgcd  16474  dfgcd2  16476  rplpwr  16488  nn0rppwr  16491  nn0expgcd  16494  lcmgcdlem  16536  lcmfunsn  16574  coprmdvds1  16582  qredeq  16587  2mulprm  16623  prmdvdsexpr  16647  nnnn0modprm0  16737  prm23ge5  16746  pcexp  16790  difsqpwdvds  16818  prmpwdvds  16835  ramcl  16960  cshwshashlem3  17028  cshwrepswhash1  17033  elrestr  17351  mreintcl  17516  mremre  17525  mrieqv2d  17564  initoeu2lem1  17940  funcestrcsetclem9  18073  funcsetcestrclem9  18088  prstr  18224  drsdirfi  18230  latnlej  18381  latnlej2  18384  acsdrsel  18468  acsdrscl  18471  mrelatglb  18485  mrelatlub  18487  isnmgm  18537  grpasscan1  18899  grpinvnz  18908  mulgneg2  19006  gsmsymgrfix  19326  f1omvdco2  19346  symggen  19368  odcl2  19463  odhash3  19474  lsmss1  19563  lsmss2  19565  efgred  19646  efgcpbl  19654  ablfacrp  19966  ablfac1eu  19973  ablfaclem3  19987  omndadd  20026  ogrpaddlt  20036  dvdsrmul1  20273  dvdsunit  20283  irredmul  20333  c0snmgmhm  20366  lmodlema  20787  psgnodpmr  21516  phlssphl  21585  lindsss  21750  lindfmm  21753  ply1scln0  22195  dmatelnd  22400  mdetdiaglem  22502  mdet0  22510  mdetunilem7  22522  slesolinv  22584  cramerimplem3  22589  cpmatpmat  22614  m2cpminvid2lem  22658  chfacfscmul0  22762  chfacfpmmul0  22766  riinopn  22812  clsndisj  22979  cnpf2  23154  hausnei2  23257  cmpcov  23293  cmpfii  23313  unconn  23333  t1connperf  23340  nrmr0reg  23653  fbfinnfr  23745  filuni  23789  alexsubALT  23955  tmdgsum  23999  cuspcvg  24205  mopni  24397  isngp4  24517  metdsre  24759  iimulcl  24850  phtpc01  24912  clmmulg  25018  cfilucfil4  25238  bcthlem5  25245  bcth  25246  bcth3  25248  itg1le  25631  itg2le  25657  bddmulibl  25757  bddiblnc  25760  dvnres  25850  cpnord  25854  dvnfre  25873  deg1ge  26020  dgr1term  26182  aaliou3lem2  26268  sincosq1lem  26423  cxpge0  26609  cxpmul2  26615  logrec  26690  logbgcd1irr  26721  sqfpc  27064  bcmono  27205  gausslemma2dlem1a  27293  gausslemma2dlem2  27295  gausslemma2dlem4  27297  2lgsoddprmlem3  27342  pntrmax  27492  qabvexp  27554  ostth2lem2  27562  nosepon  27594  nolesgn2o  27600  nogesgn1o  27602  nosepnelem  27608  nosepne  27609  nosepdmlem  27612  nosepdm  27613  nodenselem8  27620  noresle  27626  noetasuplem4  27665  noetainflem4  27669  scutbdaylt  27748  eqscut3  27754  addsuniflem  27932  ssltmul1  28074  precsexlem6  28138  precsexlem7  28139  precsexlem11  28143  sltonold  28186  onnolt  28191  n0sfincut  28270  expadds  28346  ax5seglem4  28896  axeuclidlem  28926  uhgredgrnv  29094  usgredg4  29181  nbuhgr2vtx1edgblem  29315  vtxduhgr0e  29443  vtxduhgr0nedg  29457  rusgrpropnb  29548  uspgr2wlkeqi  29612  redwlklem  29634  lfgrwlkprop  29650  2pthnloop  29695  spthonepeq  29716  pthdlem2lem  29731  crctcshwlkn0lem3  29776  crctcshwlkn0lem5  29778  crctcshwlkn0lem7  29780  crctcshwlkn0  29785  wlkiswwlks1  29831  wlkiswwlks2  29839  wlkiswwlksupgr2  29841  wwlksnext  29857  wwlksnextproplem2  29874  wspthsnonn0vne  29881  2pthon3v  29907  rusgrnumwwlk  29939  erclwwlkeqlen  29982  erclwwlksym  29984  erclwwlktr  29985  erclwwlkneqlen  30031  erclwwlknsym  30033  erclwwlkntr  30034  uhgr3cyclex  30145  upgreupthseg  30172  eupth2lem3lem4  30194  eucrctshift  30206  4cycl2vnunb  30253  nvs  30626  nvtri  30633  nmlno0  30758  nmlnoubi  30759  ubth  30836  hlipgt0  30877  ocnel  31261  elspansn2  31530  elspansn3  31535  normcan  31539  pjoml2  31574  lecm  31580  osum  31608  nmbdfnlb  32013  leopmul  32097  hstpyth  32192  cvnbtwn  32249  ssmd1  32274  ssmd2  32275  ssdmd1  32276  ssdmd2  32277  cvmd  32299  cvdmd  32300  superpos  32317  disji2f  32540  disjif  32541  disjif2  32544  preiman0  32671  padct  32681  ffs2  32690  bcm1n  32757  sgn3da  32798  s2f1  32905  archiabl  33159  slmdlema  33164  lbslsat  33602  eulerpartlemb  34355  fisshasheq  35107  cvmsdisj  35262  cvmlift2lem12  35306  satfrel  35359  satfrnmapom  35362  fmlasuc  35378  satffun  35401  satef  35408  sategoelfv  35412  lineintmo  36150  nn0prpwlem  36315  nn0prpw  36316  neibastop2lem  36353  lindsadd  37612  areacirc  37712  incsequz  37747  mettrifi  37756  ismtybnd  37806  heiborlem1  37810  rngoisocnv  37980  risci  37986  eqvrelqsel  38612  lfl1  39068  lkrlsp2  39101  omlfh3N  39257  cvrnbtwn  39269  cvrnbtwn2  39273  cvrnbtwn4  39277  cvlexch3  39330  cvlexch4N  39331  cvlatexchb1  39332  2llnne2N  39407  atcvrj0  39427  cvrat2  39428  ps-1  39476  3atlem5  39486  islln2a  39516  lplnriaN  39549  lplnribN  39550  llncvrlpln2  39556  lplncvrlvol2  39614  psubatN  39754  pmapglb2N  39770  pmapglb2xN  39771  2llnma1b  39785  paddasslem17  39835  pmod2iN  39848  pmodl42N  39850  hlmod1i  39855  atmod1i1  39856  atmod1i2  39858  llnmod1i2  39859  pclcmpatN  39900  osumcllem8N  39962  pexmidlem3N  39971  pl42lem4N  39981  4atexlem7  40074  ltrnnid  40135  cdlemc4  40193  cdleme32a  40440  cdlemeg46gfre  40531  cdlemf2  40561  cdlemg4c  40611  trlcoat  40722  tendovalco  40764  tendoeq2  40773  cdlemk36  40912  diael  41042  diatrl  41043  dicelval1stN  41187  dicelval2nd  41188  dihlspsnat  41332  dochkr1  41477  lcfrlem9  41549  mapdh8e  41783  hdmapval0  41832  hgmapval0  41891  nnadddir  42263  dvdsexpnn0  42327  incssnn0  42704  pell14qrexpcl  42860  pell14qrgap  42868  congadd  42959  acongsym  42969  acongtr  42971  dvdsacongtr  42977  jm2.19lem3  42984  jm2.19lem4  42985  jm2.26lem3  42994  onexlimgt  43236  nadd2rabex  43379  ismnushort  44294  bi13impia  44483  3impcombi  44810  ioogtlb  45496  iocgtlb  45503  iocleub  45504  icoltub  45509  iooltub  45511  limclner  45652  limsupre3lem  45733  climuzlem  45744  fsupdm  46843  finfdm  46847  elfzelfzlble  47325  subsubelfzo0  47330  m1modnep2mod  47356  m1modmmod  47362  modlt0b  47367  mod2addne  47368  iccpartigtl  47427  sqrtpwpw2p  47542  fmtnoprmfac1lem  47568  fmtno4prmfac  47576  evenltle  47721  even3prm2  47723  wtgoldbnnsum4prm  47806  bgoldbnnsum3prm  47808  bgoldbtbndlem1  47809  bgoldbtbndlem3  47811  bgoldbtbndlem4  47812  bgoldbtbnd  47813  uhgrimisgrgriclem  47934  isubgr3stgrlem7  47976  clnbgr3stgrgrlic  48024  gpgedg2iv  48071  pgnbgreunbgrlem3  48122  pgnbgreunbgrlem6  48128  upgrwlkupwlk  48144  funcringcsetcALTV2lem9  48302  funcringcsetclem9ALTV  48325  lincscmcl  48437  lindslinindimp2lem4  48466  lincresunit2  48483  lincresunit3  48486  elfzolborelfzop1  48524  rege1logbzge0  48564  fllog2  48573  dignn0ldlem  48607  rrx2pnecoorneor  48720  rrx2plord2  48727  rrx2linest  48747  ipolub  48992  ipoglb  48995